Engineering the Development of Embedded Systems - Formal Methods and Hybrid Real-Time Systems - page 394

Much of this could be addressed by developing better domain specific languages. In
fact, development systems such as MATLAB/Simulink are remarkably effective where
they apply and [Henzinger et al 2003] have shown how to add timing control to such
programs. However, where there is mixed continuous and discrete control, as in many
practical applications, this is insufficient. [Henzinger & Sifakis 2006] describe this as
the problem of combining equational and abstract computational reasoning.
Even where there is just discrete control, there are difficulties with ensuring that re-
quirements are consistent and as complete as possible. [Sukumaran et al 2006] describe
a relatively simple but very effective method of checking requirements formally by ver-
ifying that system invariants are preserved over all operations. Their method is capable
of handling practical data models in an object oriented framework. They show how to
produce visual representations of scenarios and to create prototypes that can be checked
to reveal problems.
An important part of any successful requirements definition method is the ability to
incrementally handle changes which will take place right through the design cycle of
a system. Minimizing the cost of checking that changes preserve system properties is
crucial to having the method used in practice.
Equally important is the capability to handle product lines , as most embedded sys-
tems not only incorporate code from previous versions and models but are also part of
a family of related products; changes made for one version may need to be integrated
into all versions of the product.

5 Requirements, Program Specification and Design

However well requirements are defined and checked, there remains the crucial steps
of transforming requirements into program specifications and elaborating this into a
design. These are all difficult steps and very little work has been done to formalize any
of them for a program of practical size.
It is here especially that formalizing combined discrete and continuous control poses
basic problems. While the models used for control will differ, so will the methods of
reasoning: equational and quantitative in one case and in terms of a programming logic
in the other. Henzinger and Sifakis ([Henzinger & Sifakis 2006]) describle the difficul-
ties and point out that solving them will need basic advances in computer science.
Recent work ([Sharma et al 2006, Chakravorty & Pandya 2003, Pandya et al 2007],
[Agrawal et al 2006, Agrawal & Thiagarajan 2005]) suggests that discrete sampling of
continuous systems may provide a sufficient approximation for the precise control of
mixed systems. Incorporating such techniques into a specification method will make it
possible to consider their use for practical applications.

6 Progress: Termination

A real-time program is usually designed to execute without termination. The program
will consist of a number of concurrent operations that perform different functions. So
while the program as a whole should be non-terminating, each operation of the program