Platform-independent Design for Embedded Real-time Systems

 

Introduction and Problem Statement

Real-time embedded systems have been in widespread use in various fields such as consumer, industry, commerce and military. Examples of these applications include microchip-controlled domestic appliances, medical instruments, telephone and communication systems, missile control systems, avionics and defense systems, automobile control systems and traffic control systems. Such systems can be characterized as having complex functionality, stringent timing constraints, concurrency and distribution.

 

Traditional design methods have been proven insufficient for expressing the features of real-time embedded systems. Designers have to rely on ad-hoc, bottom-up methods to implement a system. Early design decisions about e.g. architecture selection and functionality decomposition are based on inadequate analyses of the system. These early design decisions have a big impact on the correctness and performance of the final implementation. However, traditional approaches allow the verification of performance and correctness properties only at the moment the system is actually mapped onto the target platform. Therefore mistakes introduced at the early design stage are discovered late and often lead to expensive design iterations.

 

The aim of this project is to remedy the problems described above by proposing a systematic design methodology covering both system design and system generation. The methodology focuses on establishing correctness consistency (especially w.r.t. timing constraints) of the system during the complete development cycle.

 

Objectives and Research Issues

The goal of this project is to develop a design method for embedded real-time systems that helps designer to (1) quickly explore the design space, (2) evaluate design decisions with respect to performance and real-time requirements, (3) construct a well-founded design description that refrains from implementation details and (4) automatically generate correct implementation from the design description.

 

We approach the project objectives by investigating the following two issues: platform-independent design and correctness-preserving transformation from design to implementation.

 

1. Platform-independent design provides a virtual execution environment in which the design description is uniquely interpreted and executed. Thus design decisions can be formally evaluated without being affected by non-deterministic factors caused by specific platforms. Correctness and performance of design solutions can be checked formally checked by simulation and verification techniques. As a result, many design errors can be corrected at an early development stage, thereby avoiding costly and time-consuming iterations. Furthermore, the design can thus be targeted to different or modified platforms.

 

2. The correctness-preserving transformation take a design model as input, and generates a complete hardware/software implementation whose correctness is guaranteed during the transformation. In this way one can avoid performing cosly and time-consuming tests of the final implementation.

 

Both issues are closely related and essential in developing embedded real-time systems. Platform-independent design guarantees an unambiguous interpretation of the design description whose performance and correctness can be analyzed by verification and simulation techniques. Based on the analysis results, a well-founded design description can be built, which is a prerequisite for the procedure of the correctness-preserving transformation from the model to the implementation. On the other hand, without correctness-preserving transformation, a reliable and qualified implementation cannot be generated easily. The methodology attempts to address both aspects and propose a consistent approach for developing embedded real-time systems. 

 

Achieved Results

During the past two and half years, research efforts have been carried out concerning above issues. With respect to the platform-independent design, research has been focused on investigating formal models of the system and their correctness and performance evaluation. Regarding the correctness-preserving transformation, a transformation strategy has been proposed, which guarantees the correctness of the generated implementation. Initial experiments have been performed that confirm the advantages of this methodology.

 

List of Recent Publications

 

Real-time Property Preservation in Approximations of Timed Systems,
Jinfeng Huang, Jeroen Voeten, Marc Geilen,
To appear In Proceedings of  First ACM & IEEE International Conference on
Formal Methods and Models for Codesign.  June  2003,  Mont Saint-Michel, France

 

Performance Evaluation of Complex Real-time Systems: A Case Study ,
Jinfeng Huang, Jeroen Voeten, Piet van der Putten, Andre Ventevogel, Ron Niesten and Wout vd Maaden, 

In Proceedings of PROGRESS'2002, STW Technology Foundation, Oct 2002, Utreht.

 

A calculus for mobile network systems,

Jinfeng Huang, Ad Verschueren, Henri Aalderink, Johan Lukkien,

In Proceedings of 4th International Conference on Formal Engineering Methods 2002,

LNCS 2495, Springer-Verlag Berlin Heidelberg 2002.

 

Network middleware and Mobility,

P.H.F.M. Verhoeven, J.Huang, J.J.Lukkien,

In Proceedings of PROGRESS'2001, STW Technology Foundation, October 2001.

 

Utilization

The modelling method developed thus far has been applied in a number of case studies. One of the case studies concerns the performance analysis of an MA3 system. MA3 (a More Accessible Micro Assembler with a Modular Architecture) system, a universal assembler for MST production systems, is produced by TNO Industrial Technology. Due to the complexity of the system, real-time performance analysis is quite difficult using traditional methods. In “Performance Evaluation of Complex Real-time Systems: A Case Study”, our experiences with applying the POOSL language for modeling the MA3 system are presented. By evaluating the response delay of the system against the capacity (the number of processing units) of the system, proper design decisions can be made about the architecture of the system. Furthermore, by comparing the POOSL model with a rapid prototype of MA3, it shows that the POOSL model provides a low-cost and flexible solution for evaluating the performance of complex real-time systems.

 

A prototype tool that supports the transformation strategy to automatically generate a correct implementation has been implemented. Currently experiments are being carried out to apply this prototype tool for a toy control problem. In the near future we plan to apply the approach to an industrial-sized problem.