Formal specification, model checking and model-based testing are recommended techniques for engineering of mission-critical systems. In the meantime, those techniques struggle to obtain wide adoption due to inherent learning barrier, i.e. it is considered difficult to use those methods. There is also a common difficulty in translating the specifications in natural language, a common practice nowadays, to formal specifications. In this position paper we discuss the concept of an end-to-end methodology that helps identify specifications from various sources, automatically create formal specifications and apply them to verification of cyber-physical systems. Thus, we intent to address the challenges of creation of formal specifications in an efficient automated and tool-supported manner. The novelty of the approach is analyzed through a survey of state of the art. It is currently planned to implement this concept and evaluate it with industrial case studies.
Smartphones are becoming necessary tools in the daily lives of mil-lions of users who rely on these devices and their applications. There are thou-sands of applications for smartphone devices such as the iPhone, Blackberry, and Android, thus their reliability has become paramount for their users. This work aims to answer two related questions: (1) Can we assess the reliability of mobile applications by using the traditional reliability models? (2) Can we model adequately the failure data collected from many users? Firstly, it has been proved that the three most used software reliability models have fallen short of the mark when applied to smartphone applications; their failures were traced back to specific features of mobile applications. Secondly, it has been demonstrated that the Weibull and Gamma distribution models can adequately fit the observed failure data, thus providing better means to predict the reliability of smartphone applications.
Insufficient requirements reusability, understandability and verifiability jeopardize software projects. Empirical studies show little success in improving these qualities separately. Applying object-oriented thinking to requirements leads to their unified treatment. An online library of reusable requirement templates implements recurring requirement structures, offering a starting point for practicing the unified approach.
s of Invited Talks Science of Computing: From Functions and Sequentiality to Processes and Concurrency
Over the years dashboards have become an essential part of managers’ toolkit. The recent developments in the field of IT allowed companies to build complex monitoring and metric-driven solutions for their business needs. The increasing amount of complexity in these dashboards resulted in the increased cost of maintenance and further development. In addition, large corporations have experienced concerns with designing dashboards that are suitable for multiple roles within the organization, i.e. showing the appropriate metrics to people at different positions. By having a self-adjusting, adaptable dashboard, businesses would not only increase the productivity of their workers but could benefit from a fully-fledged Adaptable System (AS) that requires little to no maintenance while performing better than a manually-built and maintained dashboard. Nevertheless, such a system would have a broader set of additional requirements that will be discussed later. This paper presents the design and the architecture of types of adaptable dashboards that address the above-mentioned concerns.
The REVaMP2 Project is a major European effort towards Round-Trip Engineering of Software Product Lines for software intensive systems. Indeed, software is predominant in almost every modern industry. The importance of time-to-market has grown tremendously in many business domains. Organizations are in a constant search for approaches for mass production of highly customizable systems. The software product lines engineering approach promises to provide up to 10× speed increase benefits in time-to-market. Traditionally, automated tools proposed a top-down approach, i.e., variants were generated from a model of the product line. However, the industry used a bottom-up approach that helped to re-create a product line out of various clones of a system. This operation is very costly and error prone. The goal of REVaMP2 is to automate the process of extracting a product line from various system artifacts and help with verification and the co-evolution of the product line. The project involves 27 partners that contribute with diverse research and industrial practices to address case study challenges stemming from 11 application domains. In this paper, we would like to present the motivation for the project, the current approach, the intermediate results and challenges.
There are hundreds of companies out there that are bringing new solutions in the field of robotics and trying to get rid of a thousand problems they face. Nevertheless, most of their results do not leave the doors of the lab and remain without any decent attention from society. Institutions and companies require highly qualified personnel to accelerate the development of new solutions and products. High expenses deter broad masses from participating in this activity. It is not only the high price that keeps people away from being a part of the community but also a high entry level to the field. In our paper we consider an approach that makes the process of developing and integration of robotic systems faster and more accessible to the others. At first, the idea implies removing a technical barrier between science labs and other individuals. Secondly, all processes must be automatized by different tools to the greatest possible extent. As a result, we get a cloud web application where anyone can add or edit robotic systems algorithms. There are open technologies that can help us to implement this solution: virtualization, dockerization, web 3d simulator Gazebo, robot operation system (ROS).
In this study, the Goals Questions Metrics (GQM) approach was utilized to analyze the relationship between lifestyle and software process-oriented factors and the job satisfaction level of Software Engineers. The author organized the questionnaire that included questions addressing all the metrics identified during GQM activities. Gathered metrics are analyzed on being correlated with workplace contentment of survived developers. The author found ten statistically significant factors on a confidence interval of 95%. Those are age, deadline pressure, personality, an average number of lines of code contributed to a project weekly, relationships with peer colleagues and management, an intensity of interaction with customers, sleep duration, quality of working environment, and prevalence of agile methods in the development process in a company. However, a number of factors, that are generally believed to influence job satisfaction, were found to be insignificant. Overtime working, project criticality were demonstrated to have no considerable effect on job satisfaction. Multivariate regression was employed to build the model to recognize what metrics are the most important to assess workplace contentment. The author shows that depending on included factors it is possible to achieve R-square of 59–89%.
The electroencephalograph (EEG) signal is one of the most widely used signal in the field of computer science to analyze the electrical brain waves from software developers and students. In this paper we present initial research results of an empirical study related to application of EEG in measurement of software development activities. We discuss existing methods and problems of running such experiments in future. In particular, we focus on the different kinds of limitations implied by modern EEG devices as well as the issues related to evaluation of the collected data set.
Detecting possible weaknesses in a dynamically typed functional programming language at compile time plays an important role in the development of correct Software. Unfortunately, this is still an open problem for some functional programming languages. This paper proposes a translation of Clojure programs into Boogie. Thus, users can write formal specifications of Clojure programs, using pre- and postconditions that are supported by the language, translate the code to Boogie, and use Boogie’s automated theorem provers to formally check the correctness of the code w.r.t. its specifications. This enables users to formally prove Clojure programs enriched with pre- and post-conditions. This paper shows the translation rules, its implementation and discusses some of the challenges faced due to differences between the source and the target languages.
MegaM@Rt2 Project is a major European effort towards the model-driven engineering of complex Cyber-Physical systems combined with runtime analysis. Both areas are dealt within the same methodology to enjoy the mutual benefits through sharing and tracking various engineering artifacts. The project involves 27 partners that contribute with diverse research and industrial practices addressing real-life case study challenges stemming from 9 application domains. These partners jointly progress towards a common framework to support those application domains with model-driven engineering, verification, and runtime analysis methods. In this paper, we present the motivation for the project, the current approach and the intermediate results in terms of tools, research work and practical evaluation on use cases from the project. We also discuss outstanding challenges and proposed approaches to address them.
The number of Smartphone users in the world is expected to pass the five billion in 2019. The major credit for this exponential growth is the competition between Smartphones manufacturing companies and increasing Internet availability in the world. Processing power considered to be one of the most important features in Smartphones and it is evolving year by year. Until now, building a distributed computing system done exclusively using PCs and other server infrastructure. In this paper we will propose a new architecture for a distributed computing system consists of a network of Smartphones and use their computation power to execute machine learning models on each Smartphone. As proof of concept, our solution will provide a stable layer to execute large data-sets using common machine learning algorithms such as Linear Regression.
Face Detection and Recognition is an important surveillance problem to provide citizens’ security. Nowadays, many citizen service areas as airports, railways, security services are starting to use face detection and recognition services because of their practicality and reliability. In our research, we explored face recognition algorithms and described facial recognition process applying Fisherface face recognition algorithm. This process is theoretically justified and tested with real-world outdoor video. The experimental results demonstrate practically applying of face detection from several foreshortenings and recognition results. The given system can be used in building a smart city as a smart city application, also in different organization to ensure security of people.
Cyber resilience is the most important feature of any cyber system, especially during the transition to the sixth technological stage, and related Industry 4.0 technologies: Artificial Intelligence (AI), Cloud and foggy computing, 5G +, IoT/IIoT, Big Data and ETL, Q-computing, Block chain, VR/AR, etc. We should even consider the cyber resilience as primary one, because the mentioned systems cannot exist without it. Indeed, without the sustainable formation, made of the interconnected components of the critical information infrastructure, it does not make sense to discuss the existence of 4.0 Industry cyber-systems. In case when the cyber security of these systems is mainly focused on assessment of the incidents’ probability and prevention of possible security threats, the cyber security is mainly aimed at preserving the targeted behavior and cyber systems’ performance under the conditions of known (about 45%) as well as unknown (the remaining 55%) cyber-attacks.
Modern cyber systems acquire the more emergent system properties, as far as their complexity is being increased: cyber resilience, controllability, self-organization, proactive cyber security and adaptability. Each of the listed properties is the subject of the cybernetics research (comes from Greek κυβερνητική (kybernētikḗ) - the art of the governance) and each subsequent feature makes sense only if there is a previous one. This article presents a valuable experience and the exploratory study practical results of the Innopolis University Information Security Center on the scientific problem of the cyber-resilient critical information infrastructure organization under the conditions of previously unknown heterogeneous mass cyber attacks of intruders, based on similarity invariants. It is essential that the obtained results significantly complement the well-known practices and recommendations of ISO 22301 ( https://www.iso.org ), MITRE PR 15-1334 ( www.mitre.org ) and NIST SP 800-160 ( www.nist.gov ) in terms of developing the quantitative metrics and cyber resistance measures. This makes it possible for the first time to discover and formally present the ultimate efficiency law of the cyber resilience of modern Industry 4.0 systems under increasing security threats.
