QUAREM: Quantitative Reactive Modeling
European Research Commission, Advanced Investigator Grant
Principal investigator: Tom Henzinger
Host institution: IST (Institute of Science and Technology), Austria
Formal verification aims to improve the quality of software by detecting errors before they do harm. At the basis of formal verification is the logical notion of correctness, which purports to capture whether or not a program behaves as desired. We suggest that the boolean partition of software into correct and incorrect programs falls short of the practical need to assess the behavior of software in a more nuanced fashion against multiple criteria. We therefore propose to introduce quantitative fitness measures for programs, specifically for measuring the function, performance, and robustness of reactive programs such as concurrent processes.
The project aims to build and evaluate a theory of quantitative fitness measures for reactive models. Such a theory must strive to obtain quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction, model checking, and synthesis. The theory will be evaluated not only in the context of hardware and software engineering, but also in the context of systems biology. In particular, we plan to use the quantitative reactive models and fitness measures developed in this project for testing hypotheses about the mechanisms behind data from biological experiments.
SMSCOM: Self Managing Situated Computing
European Research Commission, Advanced Investigator Grant
Principal investigator: Carlo Ghezzi
Host institution: Politecnico di Milano, Italy
Software is the key enabling technology of our society. Since the early 1970s, there has been a continuous progress in the science and engineering of software, which led to better quality of products. Today, however, emerging requirements are challenging our current knowledge, and require a shift from the incremental improvements we have experienced in the past to radical changes to the way software is conceived, developed, and operated. In particular: Software development and operation are increasingly decentralized. Applications are composed dynamically out of parts that are developed and operated by independent parties. Requirements changes ask for continuous software adaptation and evolution. The infrastructures on which applications run are fully distributed. Technologies like RFID tags, wireless sensors, and embedded devices imply that the infrastructure can change dynamically both in physical and in logical structure. The so-called Internet of Things is fostering a situation where computing power and connectivity are not only possible any-time and any-place, but also for any-thing.
The project focuses on pervasive software that lives in a continuously changing world and in different, often unexpected, situations. The software must be able to respond to changes dependably and in a self-managed manner. All aspects of software development and operation are revisited to support these goals. The project focuses on all of them from a software engineering standpoint, stressing both rigorous methodological approaches and the development of tools and case studies, which aim at validating the methods.
VERIWARE: From Software Verification to `Everyware' Verification
European Research Commission, Advanced Investigator Grant
Principal investigator: Marta Kwiatkowska
Host institution: University of Oxford, UK
In the words of Adam Greenfield, "the age of ubiquitous computing is here: a computing without computers, where information processing has diffused into everyday life, and virtually disappeared from view". Conventional hardware and software has evolved into `everyware' – sensor-enabled electronic devices, virtually invisible and wirelessly connected – on which we increasingly often rely for everyday activities and access to services such as banking and healthcare. The key component of `everyware' is software, embedded inside electronic gadgets and continuously interacting with its environment by means of sensors and actuators. Ubiquitous computing must deal with the challenges posed by the complex scenario of communities of `everyware', in presence of environmental uncertainty and resource limitations, while at the same time aiming to meet high-level expectations of autonomous operation, predictability and robustness. This calls for the use of stochastic modelling, discrete and continuous dynamics, quantitative measures, and goal-driven approaches, which the emerging quantitative software verification is unable to address at present.
The central premise of the VERIWARE project is that there is a need for a paradigm shift in verification to enable `everyware' verification, which can be achieved through a model-based approach that admits discrete and continuous dynamics, the replacement of offline methods with online techniques such as machine learning, and the use of game-theoretic and planning techniques. The project will significantly advance quantitative probabilistic verification in new and previously unexplored directions. This will involve investigating the fundamental principles of `everyware' verification, development of algorithms and prototype implementations, and experimenting with case studies.
LUCRETIUS: Foundations for Software Evolution
European Research Commission, Advanced Investigator Grant
Principal investigator: John Mylopoulos
Host institution: University of Trento, Italy
Software evolution refers to changes made to a software system after its deployment. These changes may be caused by changing requirements, domain assumptions, or computing infrastructure, and may affect the system's implementation, architecture and/or requirements. Evolution may be automatic (aka self-adaptation), or manual, or something in-between.
This project aims to develop principles that underlie, and concepts, tools and techniques that support evolution. The project will focus on software-intensive systems. Such systems consist of software, human and organizational elements that work together to fulfill organizational and human objectives. Our proposed research is founded on ideas and research results from Requirements Engineering (RE). Evolution is to be supported by design-time models that are made available at run-time. These models capture system requirements and domain assumptions, augmented with design and implementation details. When evolution is automatic, supported by monitor-diagnose-compensate-execute feedback loops, these models determine (i) what is to be monitored, (ii) whether the system is operating according to its intended purpose, (iii) what are possible compensations for deviations from intended behaviour, (iv) how to evolve the system.
When evolution is manual, these models support evolution activities, carried out by humans, by offering a comprehensive picture of the requirements and assumptions under which the system operates, along with traceability links between elements of these models and code. This means that design-time models need to capture stakeholder intentions and commitments, social interactions, business processes, and organizational goals that ultimately determine system requirements. Expected results from the project include the development of novel concepts, tools and techniques for designing evolution-enabled software-intensive systems.
PBM-FIMBSE: Partial Behaviour Modelling: A Foundation for Incremental and Iterative Model-Based Software Engineering
European Research Commission, IDEAS Starting Grant
Principal investigator: Sebastian Uchitel
Host institution: Imperial College of Science, Technology and Medicine, UK
Software systems are amenable to analysis through the construction of behaviour models. This corresponds to the traditional engineering approach to construction of complex systems. The advantage of using behaviour models to describe systems is that they are cheaper to develop than the actual system. Consequently, they can be analysed and mechanically checked for properties in order to detect design errors early in the development process and allow cheaper fixes. Although behaviour modelling and analysis has been shown to be successful in uncovering subtle requirements and design errors, adoption by practitioners has been slow. One of the reasons for this is that traditional approaches to behaviour models are required to be complete descriptions of the system behaviour up to some level of abstraction, i.e., the transition system is assumed to completely describe the system behaviour with respect to a fixed alphabet of actions. This completeness assumption is limiting in the context of software development process best practices which include iterative development, adoption of use-case and scenario-based techniques and viewpoint- or stakeholder-based analysis; practices which require modelling and analysis in the presence of partial information about system behaviour.
The aim of this project is to shift the focus from traditional behaviour models to partial behaviour models – operational descriptions that are capable of distinguishing known behaviour (both required and proscribed) from unknown behaviour that is yet to be elicited. Our overall aim is to develop the foundations, techniques and tools that will enable the automated construction of partial behaviour models from multiple sources of partial specifications, the provision of early feedback through automated partial behaviour model analysis, and the support incremental, iterative elaboration of behaviour models.
