Formal Methods for Contracting
Final Report Abstract
The goal of research project B2 was to provide the theoretical background for contracting over multiple viewpoints in the CCC project. Before, there was no existing contracting model that supported these different viewpoints (i.e., functional and non-functional). To be able to use the defined contracts in a running system, the contracts needed to be negotiated between the corresponding components in the system. Thus, a negotiation mechanisms needed to be defined to do this automatically. Our results, derived suggestions, and provided tool support constitute a major step towards further advancements of a safe and verified update process for cyber-physical systems. Besides the multi-viewpoint contracting for component-based systems, a special scientific concern of the B2 research unit has been the seamless integration of general contracting methodologies into software engineering practices (i.e., from model-based software development to source code implementations) and their improvement. A reason is that, despite their significance, the software industry has not yet widely adopted such verification techniques as part of their software engineering processes. To address this problem, we studied and improved the paradigm of contracting in three areas. First, in close cooperation with project C2, we developed a formal concept and advanced tool support for specifying and verifying skill graphs. Skill graphs are an established means to model complex cyber-physical systems (e.g., vehicle automation systems) by distributing complex behaviors among so called skills with interfaces between them. Skills are mapped to sub-systems (i.e., connected software components) and therefore provide a more abstract view of component-based systems. Our concept establishes a starting point for a model- and refinement-based verification and engineering process that is structured and less prone to errors. Second, we introduced the concept of agile formal methods, which combines formal methods (e.g., such as deductive verification) with agile processes. Moreover, we studied how to improve the specification phase in an agile process (i.e., with frequent changes). We derived a notion of feature-oriented contracts and exhibited that there exists a connection between the goals of the B2 project and the large community of software product lines. Our results indicate that the software product line community will greatly benefit from our insights obtained in the CCC project. Third, we conducted studies on how to improve external configurable verification tools. We argue that a better understanding of parameterization allows tool builders to better support users of deductive verification. In particular, we investigate whether specific parameters have a larger influence on automated provability and whether specific options increase or decrease the verification effort. Our results are particularly significant for resource-constrained applications, as we can find smaller proofs, and non-experts, as tool interaction is decreased. Our empirical insights give tool builders a comprehensive understanding of their control parameters. In summary, our contributions constitute a major leap towards automated deductive verification and better applicability of verification tools for non-experts.
Publications
- Proof-Carrying Apps: Contract-Based Deployment-Time Verification. In Proc. of the International Symposium on Leveraging Applications (ISoLA), pages 839–855, Berlin, Heidelberg, October 2016. Springer
S. Holthusen, M. Nieke, T. Thüm, and I. Schaefer
(See online at https://doi.org/10.1007/978-3-319-47166-2_58) - Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates. In Proc. of the PrePost workshop co-located with IFM, 2016: 31-45
S. Holthusen, S. Quinton, I. Schaefer, J. Schlatow, M. Wegner
(See online at https://doi.org/10.4204/EPTCS.208.3) - Modularization of Refinement Steps for Agile Formal Methods. In Proc. of the International Conference on Formal Engineering Methods (ICFEM). 2017
F. Benduhn, T. Thüm, I. Schaefer, and G. Saake
(See online at https://doi.org/10.1007/978-3-319-68690-5_2) - Experience Report on Formally Verifying Parts of Open-JDK's API with KeY. In Fourth Workshop on Formal Integrated Development Environment (F-IDE), July 2018
A. Knüppel, T. Thüm, C. Pardylla, and I. Schaefer
(See online at https://doi.org/10.4204/EPTCS.284.5) - Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. In 9th International Conference on Interactive Theorem Proving (ITP), Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 2018
A. Knüppel, T. Thüm, C. Pardylla, and I. Schaefer
(See online at https://doi.org/10.1007/978-3-319-94821-8_20) - Feature-Oriented Contract Composition. In Journal of Systems and Software (JSS), Elsevier, 2019
T. Thüm, A. Knüppel, S. Krüger, S. Bolle, and I. Schaefer
(See online at https://doi.org/10.1016/j.jss.2019.01.044) - Skill-Based Verification of Cyber- Physical Systems. In 23rd International Conference on Fundamental Approaches to Software Engineering (FASE'20), 2020
A. Knüppel, I. Jatzkowski, M. Nolte, T. Thüm, T. Runge, and I. Schaefer
(See online at https://doi.org/10.1007/978-3-030-45234-6_10)
