EVAS: Verification of Adaptive Systems

Project Topic

Development methodology for verifiably adaptive embedded systems.

Project Description

The goal of the project is the development of new methods for modeling, analysis, and model-based synthesis of embedded systems that support dynamic adaptivity. We call a hardware-software system adaptive, if it can adapt its behavior and architecture to changing requirements of the environment. Since adaptions can affect different subsystems in parallel, techniques are needed that guarantee the correct functioning of the overall system at any point in time. A central topic of the project is the integration of modeling, design, analysis, verification, simultation, and testing methods for adaptive systems. In particular, we address the following areas of research:

• Languages for modeling of adaptation
• Quantitative safety and dependability analysis
• Analysis and verification of safety properties of adaptive system models
• Model-based synthesis from adaptive system models
• Implementation verification of adaptive systems
• Concepts for adaptive architectures

Project Members

Project Chair

• Prof. Dr. Peter Liggesmeyer
• Prof. Dr. Klaus Schneider
• Prof. Dr. Arnd Poetzsch-Heffter

Participating Research Groups

• Fraunhofer Institute for Experimental Software Engineering (IESE)
• Reactive Systems Group, Department of Computer Science
• Software Technology Group, Department of Computer Science

Scientific Personnel

• Mario Trapp (Fraunhofer Institute for Experimental Software Engineering (IESE))
• Rasmus Adler (Fraunhofer Institute for Experimental Software Engineering (IESE))
• Jan Olaf Blech (Software Technology Group)
• Ina Schaefer (Software Technology Group)
• Tobias Schüle (Reactive Systems Group)

External Cooperation

Project Events and Achievements

The project started on October, 1st 2005, and runs until December, 31st 2007.

Project Milestones

February 2006

Project meeting on benchmark examples

March - June 2006

Several internal meetings to discuss GME modelling language, translation to formal modelling framework and GME modelling of Concept Car benchmark example.

March-June 2006

Development of formal semantic-based modelling framework for synchronous adaptive systems (SAS) serving as mediator level between GME modelling tool (Fraunhofer Institute for Experimental Software Engineering (IESE)) and AVEREST modelchecker (Reactive Systems Group)

July 2006

Report on formal modelling framework and specification logic for synchronous adaptive systems (SAS) with first directions towards verification (available at http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=699)

July 2006

Project meetings to discuss progress and further directions of collaboration

August 2006

Meeting to discuss benchmark scenario for demonstrator ConceptCar capable to show the integration of the different approaches of the participating groups

August - November 2006

Implementation of Translation from GME-XML output to Katja-based representation of formal SAS models

October 2006

EVAS Project Meeting to discuss current status and integration of functionality into adaptive models by using pre-post-condition specifications

October - December 2006

Implementation of Quartz code generation from SAS models

November - December 2006

Investigation of benchmark examples (Concept Car, Light Control Scenario et al. ) for development of verification techniques, in particular property-preserving abstraction and decomposition

January - March 2007

Integration of translations from GME-XML to SAS Models and of Quartz code generation from SAS models into AMOR tool which prototypically implements formal intermediate layer for verification, Implementation of simple property-preserving abstractions, First framework for proving transformations correct

January - April 2007

Verification of generic and application specific properties of Light Control Scenario as first benchmark for integration of all approaches applied in the EVAS project, Development of specialised verification techniques for system stability

April - July 2007

Development of theoretical foundations for SAS Model transformations for reduction of verification complexity, Transformations are proved correct by translation validation and automatic proof generation in AMOR Tool

May - June 2007

Development of specialised verification procedures for stability of adaptation

from August 2007

Further Development of AMOR Tool: Development and Implementation of complex property-preserving model transformations and abstractions for SAS models

* Benchmark Example: Traction Control *

April - June 2007

Development of GME Model and application specific property list for ConceptCar Traction Control Scenario

May - July 2007

Verification of generic adaptive properties in Traction Control Scenario

August 2007

ConceptCar hardware is fully functional and production code for Traction Control Scenario can be generated.

July - December 2007

Verification of complex adaptive and functional properties in Traction Control Scenario (using Model Transformations, Abstractions and Decompositions)

from August 2007

Generation of production code for Traction Control Scenario for ConceptCar from verified models of adaptation behaviour

Presentations

• K. Schneider and T. Schuele presented the Averest framework at the Workshop on "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" in Dresden, Germany, February 2006.

• I. Schaefer presented paper on "Formal Modelling Framework for Embedded Adaptive Systems" at the Workshop on Trustworthy Software in Saarbrücken, Germany, May 2006. (Slides)

• T. Schuele presented paper on "Verifying the Adaptation Behavior of Embedded Systems" at the Workshop on Software Engineering for Adaptive and Self-Managing Systems (SEAMS) at ICSE in Shanghai, China, May 2006.

• K. Schneider presented paper on "Efficient Code Generation from Synchronous Programs" at the Conference on Formal Methods and Models for Codesign (MEMOCODE) in Napa Valley, CA, USA, July 2006.

• E. Vecchié presented paper on "Modular Compilation of Synchronous Programs" at the Conference on Distributed and Parallel Embedded Systems (DIPES) in Braga, Portugal, October 2006.

• T. Schüle presented paper on "Verification of Data Paths Using Unbounded Integers: Automata Strike Back" at the Haifa Verification Conference (HVC) in Haifa, Israel, October 2006.

• I. Schaefer presented brief annoucement on "Towards Modular Verification of Stabilization in Self-Adaptive Embedded Systems" at 8th Intl. Symposium on Stabilization, Safety and Security of Dirstibuted Systems (SSS'06) in Dallas, TX, November 2006. (Slides)

• J. O. Blech presented paper on "Translation Validation for System Abstractions" at the 7th Intl. Workshop on Runtime Verification (RV'07) in Vancouver, Canada, March 2007. (Slides)

• EVAS project was presented at DASMOD Workshop on Verification of Adaptive Systems (VerAS'07) on September 14, 2007 - (Rasmus Adler's Slides) (Ina Schaefer's Slides) (Tobias Schüle's Slides)

• I. Schaefer presented EVAS joint paper on "From Model-based Design to Formal Verification of Adaptive Embedded Systems" at 9th Intl. Conference on Formal Engineering Methods (ICFEM'07) in Boca Raton, Florida, 14 - 15 November 2007 (Slides)

• I. Schaefer presented joint paper on "Model-based Development of an Adaptive Vehicle Stability Control System" at "Modellbasierte Entwicklung eingebetteter Fahrzeugfunktionen" held jointly with Modellierung 2008 in Berlin, March 14 2008 (Slides)

Project Publications

Slicing for Model Reduction in Adaptive Embedded Systems Development

Ina Schaefer, Arnd Poetzsch-Heffter. In: Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2008), Leipzig, Germany. May, 2008

Model-based Development of an Adaptive Vehicle Stability Control System

Rasmus Adler, Ina Schaefer, Tobias Schüle. In: Workshop "Modellbasierte Entwicklung von eingebetteten Fahrzeugfunktionen", Modellierung 2008, Berlin, March 2008. March, 2008

Probabilistic assessment of safety-critical adaptive systems, considering signal delays and cycles

Rasmus Adler, Dominik J. Domis, Marc Förster, Mario Trapp. In: The 54th Annual Reliability & Maintainability Symposium (RAMS), Las Vegas, Nevada, USA. January, 2008

From Model-Based Design to Formal Verification of Adaptive Embedded Systems

Rasmus Adler, Ina Schaefer, Tobias Schüle, Eric Vecchié. In: 9th International Conference on Formal Engineering Methods (ICFEM 2007), Boca Raton, FL. LNCS, Springer, November, 2007

Development of Safe and Reliable Embedded Systems using Dynamic

Rasmus Adler, Daniel Schneider, Mario Trapp. In: 1th Workshop on Model-driven Software Adaptation M-ADAPT at ECOOP, Berlin, Germany. July, 2007

Translation Validation for System Abstractions

Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter. In: 7th Workshop on Runtime Verification (RV'07), Vancouver, Canada. to appear, March, 2007

Runtime Adaptation in Safety-Critical Automotive Systems

Mario Trapp, Rasmus Adler, Marc Förster, Janosch Junger. In: The IASTED International Conference on Software Engineering (SE2007), Innsbruck, Austria. Februrary, 2007

Verification of Data Paths Using Unbounded Integers: Automata Strike Back

Tobias Schüle, Klaus Schneider. In: E. Bin and A. Ziv and S. Ur ed., Haifa Verification Conference (HVC), Haifa, Israel. LNCS, Volume 4383, Springer, P. 65-80, 2007

Determining Configuration Probabilities of Safety-Critical Adaptive Systems

Rasmus Adler, Marc Förster, Mario Trapp. In: IEEE International Symposium on Ubisafe Computing (UbiSafe'07), Niagara Falls, Canada. IEEE Computer Society, 2007

Towards Modular Verification of Stabilisation in Self-Adaptive Embedded Systems

Ina Schaefer, Arnd Poetzsch-Heffter. In: Eighth International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS'06), Dallas, Texas. LNCS, Volume 4280, Springer, P. 584--585, Brief Announcement, November, 2006

Physical Domain Modeling for the Development of Dependable Embedded Systems

Dominik J. Domis, Christian Schäfer, Mario Trapp. In: 10th IASTED Intl. Conference on Software Engineering and Applications, SEA2006, Dallas, TX, USA. available from http://www.actapress.com/PaperInfo.aspx?PaperID=28947, November, 2006

Modular Compilation of Synchronous Programs

Klaus Schneider, Jens Brandt, Eric Vecchié. In: 5th IFIP Conference on Distributed and Parallel Embedded Systems (DIPES 2006), Braga, Portugal. October, 2006

Efficient Code Generation from Synchronous Programs

Klaus Schneider, Jens Brandt, Eric Vecchié. In: Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06), Embassy Suites, Napa, California. July, 2006

Verifying the Adaptation Behavior of Embedded Systems

Klaus Schneider, Tobias Schüle, Mario Trapp. In: Workshop on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). ACM, May, 2006

Using Abstraction in Modular Verification of Synchronous Adaptive Systems

Ina Schaefer, Arnd Poetzsch-Heffter. In: Proceedings of "Workshop on Trustworthy Software", Saarbrücken, May 18-19, 2006. Dagstuhl Online Proceedings , available at http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=699, May, 2006

A Verified Compiler for Synchronous Programs with Local Declarations

Klaus Schneider, Jens Brandt, Tobias Schüle. In: Electronic Notes in Theoretical Computer Science (ENTCS). Volume 153, Number 4, Elsevier, P. 71-97, 2006

Bounded Model Checking of Infinite State Systems

Tobias Schüle, Klaus Schneider. In: Formal Methods in System Design (FMSD). Volume 30, Springer, P. 51-81, 2006

A Framework for Verifying and Implementing Embedded Systems

Klaus Schneider, Tobias Schüle. In: B. Straube and M. Freibothe ed., Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. Fraunhofer Institut für Integrierte Schaltungen, P. 242-247, 2006