Embedded Systems, Operating Systems

So far, the ForTesSE Group has prior experience with modeling and verification involving the verification of system-level code close to the hardware-layer, as is typical for operating systems or embedded systems.

This involves the generation of tests from models to validate models comprising assumptions on the underlying hardware, i.e. the environment. The purpose of validation scenarios is the compare a system with a model by running the tests generated from the model against the concrete system up to the point when sufficient confidence in the model has been established. The environment-model can then be integrated as basis into other verification techniques or for documentation purposes in certification processes.

The group follows two different approaches, an architecture-oriented as well as an model-based approach to specification and testing.

The research in the recently started EU IP project  https://www.euromils.eu/ is architecture-oriented, i.e. a functional and a security model of a concrete real-time operating system is directly modeled and tested in Isabelle together with industrial partners in the automotive and aerospace domain. The project aims at the certification of the real-time operating system PikeOS wrt. Common Criteria Level EAL6 and higher. The ForTesSE group is involved in WP 3 / Formal Methods, where it contributes its expertise and tools for modeling and testing techniques in order to link models and software/hardware systems via tests and to provide machine-checked documents for them. As modeling language, generic Isabelle/HOL and the HOL-TestGen System is used.

In contrast, the research in a collaboration with the IRT System X is model-based, i.e. oriented towards modeling- and test-tools that were developed for specific languages and notations used in the domain of embedded systems such UML, OCL, SysML, and SCADE. However, in order to develop and improve the tools, and in particular testing tools as a means of verification of „real-world imple­men­tations“ against models, a thorough investigation of the semantics of these languages and their combinations has to be provided. On this basis, optimizations can be based on derived rules and symbolic computations, which help to tackle with the inherent state-space explosion of these techniques in a semantically consistent way. This approach of semantics-based tool-development has already been used to construct a number of UML-related tools.  A certain emphasis is put on user-friendlyness, i.e. deep integration into the Isabelle/PIDE framework including support for model visualizations.

 


People

  • Burkhart Wolff
  • Abdou Feliachi 
  • Yakoub Nemouchi
  • Frederic Tuong
  • Achim Brucker

Papers

[8]Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler. /Journal of Automated Resoning (JAR)/, 44(1-2):111-144, 2009.
[10]Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff. Proving Fairness and Implementation Correctness of a Microkernel Scheduler. /Journal of Automated Reasoning (JAR)/, 42(2-4):349-388, 2009. G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008).
[13]Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, and Burkhart Wolff. A verification approach for system-level concurrent programs. In /Verified Software: Theories, Tools, Experiments/, LNCS 5295, pages 161-176. Springer Berlin / Heidelberg, September 2008.
[38]Achim D. Brucker and Burkhart Wolff. A verification approach for applied system security. /International Journal on Software Tools for Technology Transfer (STTT)/, 7(3):233-247, 2005
[BW12] A. Brucker and B. Wolff: On Theorem Prover-based Testing. In Formal Aspects of Computing (FAOC). DOI: 10.1007/s00165-012-0222-y. Springer, 2012.
[BW09] A. Brucker and B. Wolff: Semantics, Calculi, and Analysis for Object-Oriented Specifications. In Ernst-Rüdiger Olderog (Ed): Acta Informatica. DOI: 10.1007/s00236-009-0093-8. 46 (4), pages 255-284. Springer, 2009.
[BW08] A. Brucker and B. Wolff: An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. Journal of Automated Reasoning (JAR), DOI: 10.1007/s10817-008-9108-3, 41 (3-4), pages 219-249. 2008.
[BKLW10] A. Brucker, M. Krieger, D. Longuet, and B. Wolff. A Specification-based Test Case Generation Method for UML/OCL. In Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010), 2010. LNCS 6627.
[BW12] A. Brucker, B. Wolff: Featherweight OCL - A study for the consistent semantics of OCL 2.3 in HOL. Proceedings in the OCL2012 Workshop, Dresden. 2012. http://st.inf.tu-dresden.de/OCL2012/preproceedings/17.pdf.


You are here Application Domains Embedded Systems