Extending applicability of formal models of embedded and real-time systems

PhD: Ulrik Nyman

1. Purpose of the Project
The purpose of the project is to:

• Extend the applicability of formal models of embedded and real-time systems.
  This is done by using them in different approaches to solve problems in areas relating to embedded and real-time software development. In the PhD project the following types of models are covered:
• Embedded Systems: Input/Output Automata and State/Event Systems
• Real-Time Systems: Timed Automata and Timed Input/Output Automata

The following problem areas are the ones in which we try to extend the applicability of formal models:

• Code generation
• Development methodology
• Verification/Model Checking

The PhD project thus covers the different combinations of problem area and type of system, embedded or real-time.

2. Background
All of these topics are related to the use of formal models in the development of both embedded systems and real-time systems. The first work that was carried out as part of the PhD project was concerned with code generation in relation to software product lines[Ref]. In this setting one has a number of related embedded software products that share a lot of common functionality. Our idea is to generate code for each of the software products from one general model, containing all the functionality, and use environment specifications to describe the difference between the software products. Using Environment Specifications in this way forces the developer to give “Rely” properties of the environment in which the software will operate. The intended advantages of this approach is that the amount of modeling that the developer needs to do should be reduced. This advantage is especially relevant if an error is found in some of the common functionality, then this error only needs to be corrected in one model instead of in many models/many pieces of code.

This work subsequently lead to the work on Interface Specifications. In this work the developer is presented with a component based development methodology. In this setting the different modules that the developer creates are each others environments. In this setting it is important to reason both about the “Rely” and the “Guarantee” properties of each component, or more specifically its interface. This approach is strongly related to the work of Luca de Alfaro and Thomas Henzinger on Interface Automata [AH04,AHS02]. Such a component based development methodology presents itself to a compositional checking of whether the different interfaces respect each others assumptions.

Another compositional aspect of the work, that is part of the PhD project, is that of Compositional Backwards Reachability (CBR) [LABHKL98] which uses a compositional approach to model check properties of a given system in a backwards manner. Compositional model checking aims at exploiting properties of certain types of models in order to model check them more efficiently. If a given property can be verified by checking only part of the model, then this can be significantly faster than checking the complete model in a more direct fashion.

3. Perspective
The project aims at producing results in different but related areas. The following table gives an overview of the expected result of the project. The notation (Article 1) refers to the articles listed below the table.

Problem Area:	Code Generation	Development Methodology	Verification/Model Checking
Approach:	Environment Specifications/ Color-blindness	Interface Specifications	Compositional Backwards Reachability (CBR)
Embedded Systems Input/Output Automata State/Event Systems	An article (Article 1) already exists on the method.   An implementation should be constructed and an article (Article 7) written about the implementation.	An extended version of (Article 2) is under way describing the method.   An  implementation should be constructed and an article (Article 8) written about the implementation.	The main work here has already been done [LABHKL98]   The method should be extended to more efficient verification with queues. (QCRR) (Article 4)
Real-time Systems Timed Automata Timed Input/Output Automata	An article (Article 5) should be written on how to do optimized code generation for real-time systems given an environment context.	Work should be done on extending the method to timed systems and an article (Article 6) should be written.   An implementation could be constructed and an article (Article 9) written about the implementation.	Some work has already been done on adapting CBR to Timed Automata in my Master Thesis [UL02]   Work should be done on adapting CBR to Timed Input/Output Automata [GV04] and an article (Article 3) should be written.

Articles that are part of or are going to be part of the project:

1. Color-blind Specifications for Transformations of Reactive Synchronous Programs
2. Interface Input/Output Automata: Splitting Assumptions from Guarantees
3. Compositional Backwards Reachability for Timed I/O Automata
4. Compositional Backwards Reachability with Queues: Exploiting Repeating Patterns
5. Environment Specialization for Timed I/O Automata
6. Timed Interface Automata: Splitting Assumptions from Guarantees
7. Interface Code Generation: Generating Code from System Specifications and their Interfaces
8. Checking Interfaces: Implementation of Interface Algorithms
9. Checking Timed Interfaces: Implementation of Timed Interface Algorithms

4. Industrial Application
The project is not directly aimed at industrial application of the results. Nevertheless there are many possible application of the results. The expected results can be divided into three groups, given by the columns of the table above.

The first column represents the possibility of providing the developer of respectively embedded or real-time software with a tool which could make the software modeling easier in conjunction with automatic code generation.

The second column presents the possibility of creating a complete framework in which properties of a complete system, be it embedded or real-time, can be derived from the properties of the individual components.

The third column presents the possibility of providing more efficient verification algorithms for specific types of systems.

5. Timetable for the Project

Fall 2004

Work on the Color-blind concept and on the article for FASE 2005. (Article 1)

Spring 2005

Initial work on the QCBR method. (Postponed)

Work on extending the Color-blind concept to a general interface theory. (Lead to Article 2)

Fall 2005

Extending the theory behind Interface Specifications for Input/Output Automata (Article 2)

Planned: December, beginning work on CBR for Timed Input/Output Automata (Article 3)

Spring 2006 - Planned

Work on CBR for Timed Input/Output Automata (Article 3)

Work on an implementation of the Interface Specifications work. (Article 8)

Fall 2006 - Planned

Work on an implementation of the code generation for embedded software product lines (Article 7)

Work on adapting the color-blind concept for timed systems (Article 5)

Spring 2007 - Planned

Work on extending the Interface Specifications framework to timed systems (Article 6)

Work on QCBR (Article 4)

Fall 2007 (Until  6th of November 2007) – Planned

Work on an implementation of the Interface Specification framework for timed systems (Article 9)