Outline of the Project
Approach
Reactive systems are computer systems that continuously react to their environment at a speed determined by this environment. Most industrial ``real-time'' systems are reactive --- control, supervision and signal-processing systems. Such systems become critical players in our everyday environment, and constitute an industrial stake of increasing importance.
If we review the available, classical design tools, we find on one hand, multitasking systems driven by a real-time Operating System, and, on the other hand, general-purpose concurrent languages such as ADA. The former do not supply an acceptable level of reliability, because they do not provide a global and formal view of the system, which is separated into tasks and calls for services provided by the operating system; furthermore, they do not preserve application determinism. The latter are intrinsically non-deterministic and do not provide the necessary accurate real-time capabilities.
Synchronous languages [7, 5, 27] have been specifically designed to ease the programmer's task when dealing with reactive systems. Their basic choice is to provide idealised primitives for concurrency and communication: a reaction to an input event is considered to be instantaneous, thus making output strictly synchronous with input. For instance, the Esterel statement ``every 60 SECOND do emit MINUTE'' emits a signal ``MINUTE'' which is exactly synchronous with each 60th reception of a signal ``SECOND''. Synchronous languages offer a logical notion of concurrency, i.e., synchronous concurrency is just a way to logically split the description of an application into a set of communicating processes. This is extremely useful for describing complex systems, but has nothing to do with an actual concurrent implementation. Interaction between concurrent components within the program is conceptually performed by broadcasting events in no time and in a fully deterministic way: when a process emits a signal, the signal is instantaneously perceived by any other process which listens to it. Notice that this non-symmetric communication is exactly what is needed for reactive systems; in particular, it accurately models how a system receives events from its environment, without being able to control the speed of the environment [There is a design error in several published versions of the popular ``railroad-crossing'' example: when the gate is moving up, it does not perceive the approach of a new train. Now, if the communication is by rendez-vous, the model does not show the error: conceptually, the gate stops the train just by refusing the rendez-vous!] .
In practice, synchrony is the assumption that the program reacts rapidly enough to perceive all the external events in suitable order and to produce all the outputs for an input before reacting to a new input. For instance, automatic controllers are commonly programmed as an infinite loop over a body consisting of acquiring inputs, performing internal computations and returning outputs, execution of the body being considered atomic. This is readily abstracted into a perfectly synchronous reaction. If practical synchrony is satisfied --- and, more importantly, if its satisfaction can be checked --- the conceptual synchrony hypothesis is rather a more realistic abstraction than ignoring size limitations in the representation of numbers inside a particular computer.
Although the synchrony hypothesis may look relatively new for software, it is well-known in other fields: it is a very common assumption in digital hardware design, there called the zero-delay model; it is routinely used in control theory, where one always neglects the cost of numerical computations when designing control laws.
We don't mean that synchronous languages are the panacea for programming all real-time systems: there exist systems which are intrinsically distributed and asynchronous, and the design of complex systems generally require to deal with some degree of asynchrony. However, our claim is that one should stay in the synchronous world as long as it works, since it makes all the tasks dramatically simpler and safer.
Three synchronous languages have been designed in France during the last decade: Esterel [15] is an imperative language, while Lustre [28] and Signal [36] use a data-flow approach. An other formalism, Argos [40], inspired both by Esterel and the Statecharts, has been studied more recently. Academic research is now also taking place in European institutions like GMD and Linköping University. Corresponding research is also active in the USA, in universities like Berkeley, Austin, Carnegie Mellon, and institutions like AT&T Bell Labs and Xerox PARC. The proximity of synchronous reactive system theory with the general purpose of computer-aided design and synthesis of hardware circuits makes it an economically challenging topic worldwide. Potential impact of synchronous languages in the important area of hardware/software codesign is amply recognised by experts from this scientific community [see, for instance, the frequent references to synchronous languages in ``Hardware/software co-design. Proceedings of the NATO Advanced Study Institute, Serie Applied Sciences vol. 310, June 19-30 1995.''] .
These languages have been developed in tight cooperation. In particular, there is an important attempt to keep their compilers compatible, through the use of common formats. The goal is to translate the various languages into a single format, so as to allow various tools to be shared, and also to make easier the integration of components written in different formalisms. A first, low-level, common format, called OC (for ``object code'') was proposed a long time ago, and mainly shared by Esterel and Lustre. More recently, it was proposed to design a higher-level format. Made of two nested levels, called DC (for ``declarative code'') and DC+, this format was designed in the framework of the EUREKA-SYNCHRON project, and is intended to be used by industrial tools.
Synchronous languages are already exceptionally successful in industry, compared to other formal methods: industrial programming environments are available, and used in actual software production. For instance, Schneider-Electric uses the Saga-Lustre environment for designing systems for nuclear power-plant control and supervision. The SAO+ environment, also based on Lustre, has been chosen by Aérospatiale for the specification and maintenance of Airbus flight-control software. SAO+ is also used by VOLVO and SAAB Military Aircraft, and is likely to become a major development tool of the whole European avionics industry. Successful experiments with Esterel have taken place in several companies (in particular Dassault-Aviation and AT&T [ see, for instance, ``L.J. Jagadeesan, C. Puchol, and J.E. Von Olnhausen. A formal approach to reactive systems software, a telecommunications application in Esterel. In Formal Methods in System Design, vol. 8, pp. 123--151, 1996.'' ] ), and the language is a serious candidate to be used for designing hardware controllers by major CAD companies in the USA. Signal is used at Snecma and Thomson-Multimedia, and is under evaluation at EdF, Thomson, Siemens and VTT, among others.
These first industrial successes have prompted a demand for research extensions, from actual users. Such specific extensions are in the focus of the present proposal, which should provide new results, as well as tools ready for technology transfer, as outlined below.
The main needs for extension expressed by users concern the following areas [From now on, work areas are numbered in a uniform way. Work Area 0 will be ``Project Management'', and Work Area 1 concerns ``Case Studies Analysis''.] , which will be detailed in the next section:
- 2.--Combination of formalisms
- 3.--Program validation and verification
- 4.--Code distribution and multi-tasking
- 5.--Integrating synchrony and asynchrony
- 6.--Connection with hardware/software codesign
- 7.--Integration of analog and discrete synchronous design
As it often happens, this structure is somewhat arbitrary, and some of the considered areas are overlapping: verification will not be addressed only in area 3, but also in area 5, for mixed synchronous/asynchronous systems, and in area 7, for mixed analog/discrete systems. Code distribution has obviously to do with asynchrony. Combination of formalisms is useful in verification (expression of properties by observers) and for hardware description.
Areas 1, 4, and 6, all concern integration of models and extension outside the strict synchronous framework. As such integration/extension represents a significant part of our objectives, let us comment further on it:
The engineering of embedded systems, let it be for control or signal processing, is concerned with several types of models of quite different nature. A taxonomy of models is given in Figure below, with time and state as coordinates, either being discrete of continuous.
All synchronous formalisms assume time to be discrete but differ with regard to the modeling of state. Available synchronous formalisms are either imperative, supporting discrete state transitions, or are declarative, supporting continuous state transition, where subsystems may run on a wide variety of clock rates. Hence a combination of these formalisms (area 2) will permit to explore the full design space of discrete time models in a uniform way. Extensions towards asynchronous environments (area 5) will enter the continuous-time/discrete-state domain, while integration with analog models (area 7) will cover the last square.
This ``horizontal'' exploration of the design space is complemented by a ``vertical'' integration concerning the development process: multiparadigm design needs to be complemented by respective technology for validation and verification (area 3) if, but not only if, dealing with safety-critical applications. Further, synchronous designs have to be efficiently mapped to different target architectures with quite different goals in mind; on one hand, synchronous programs will be mapped to or integrated with real-time operating systems by adding some kind of asynchrony while essentially retaining synchrony (area 5) and still supporting real-time analysis, and on the other hand, time-critical requirements demand mapping to an architecture which combines software components and dedicated hardware components (area 6).
All these research areas are inherently linked, though addressing different topics: e.g. code distribution and multi-tasking relies on a clear understanding of the interaction of synchrony and asynchrony as investigated in area 5 and on validation/verification principles relating synchrony and asynchrony for a correct mapping to a target architecture. Or, hardware/software codesign will take advantage of the combination of different synchronous formalisms each of which is best-suited to specify particular kinds of, e.g., hardware structure. Or, particular verification methods are better-suited for particular synchronous formalisms, so that the combination of formalisms will support a combination of verification methods, and conversely, a combination of verification methods will support a multiparadigm design.
Finally, let us explain why some important topics are not addressed by the project:
- Fault-tolerance is surely a fundamental concern for
critical embedded systems. However, we are not able, by now, to
identify either problems or solutions, in this area, specific
to the synchronous approach. As the project is focused on the
synchronous approach, we deliberately leave the issue open.
- Quantitative time modelling is approached in
areas 3 and 7. However, we don't intend to develop
tools to check the well-foundedness of the synchrony hypothesis,
i.e., to evaluate the maximum reaction time of a given synchronous
program on a given machine. The reason is twofold: on a centralised
implementation, this does not seem to necessitate ``long term
research'', and the attempts to implement synchronous programs on
distributed architectures (area 4) don't seem mature enough,
by now, to start a general research on timing evaluation
[However, significant results have been obtained in this
area by the tool SYNDEX of INRIA. See, for instance ``N. Ghezal, S.
Matiatos, P. Piovesan, Y. Sorel, and M. Sorine. Un
environnement de programmation pour multiprocesseur de traitement du
signal, Research Report nr. 1236, INRIA, 1990.'']
. However, the fact that the timeliness of an implementation
be precisely measurable is an important concern in code distribution
(area 4)
Most of the proposed tasks will result in prototype tools. The adequacy of these tools to practical needs will be searched, through their assessment by users and their confrontation to actual case studies.
As far as possible, tools will be developed around existing common formats, with limited extensions only if necessary. This will make such tools independent from particular languages, and promote cross-distribution amongst project partners. This will also ease their transfer into industrial environments developed by software manufacturers aware of these representation formats.
Benefits will be immediate for industrial partners inside the project or from the Steering Committee, who will have definite influencial opportunities by expressing their needs and expectations through their submitted case studies. On a larger scale the results of the project will certainly be valuable in the framework of Esprit Workprogramme 1: Software Technology, concerning Tasks 1.1 (for embedded and safety critical systems), 1.3 and 5.5 (for hardware/software codesign).
Full partners will conduct research in coordination to propose adequate solutions to the topics mentioned above. Research will generally encompass basic aspects, but will be driven towards the development of tools applicable to industrial case studies.
Industrial associate partners, who are already familiar with synchronous languages, will provide real and significant case studies, to assess the results of the project. Some of these case studies have already been identified (see Section on case studies ).
The project will also be advised by an Industrial Steering Committee, that includes representatives of some of Europe's leading developers of embedded reactive systems.
The industrial associate partners and the members of the steering committee will make sure that the techniques and tools developed in the project are those which are the most urgently needed in industrial applications.
The main difference between the industrial associate partners within SYRF, and those who are only members of the Steering Committee lies in their degree of commitment to providing industrial case studies to full partners of the project. The industrial associate partners within SYRF have the obligation to supply the project with relevant case studies, to be available to discuss the details of the problems they propose, and to assess carefully the merits of the proposed solutions. Those who are only members of the Steering Committee are only encouraged to do so, and they are free to determine the amount of time they will invest in discussing with the SYRF partners.
Notice that none of the associate partners is a vendor of synchronous technology. The reason is that the companies that presently industrialise synchronous environments are not involved in long term research --- while being directly interested in the results and ready to transfer them. Rather, associate partners are final users of synchronous technology, who can better identify the actual needs, propose case studies, and assess the results.
As mentioned before, most research actions in the project will be assessed by applying the results on industrial case studies. Some of these case studies have already been identified (see below), but we expect other examples to be submitted by members of the Steering Committee. A very first task (hereafter called ``Work Area 1'') of the project will be that each partner get acquainted with the proposed case studies, and that these case studies be allocated to work areas and tasks. The treatment of case studies in the framework of each task is not part of this Work Area 1, but the assessment of this treatment by the associate partners is.
This case study is proposed by Schneider Electric. It concerns a ``turbine bypassing unit'' (TBU) which is a part of a nuclear protection system.
The roles of the TBU are:
- the management of a gate to the atmosphere, which has to regulate the steam pressure in the secondary circuit of the protection system, when the turbine is no longer able to maintain a superpressure.
- the computation of the nuclear power, as an image of the steam pressure.
- values of steam pressure (redundant)
- values of emergency stopping reports
- informations from testing commands of protection chain disactivation
- autotest results
- information from the supervision post
- computation parameters
- analogic values of normal command, emergency, and gate regulation.
- the analogic value of nuclear power
- switching orders
The analogic chain performs consistency controls about pressure values sampled in redundancy 3, using a voltmetric balance protecting against the drift of analogic values. One value amongst 3 is extracted. This steam pressure is integrated by means of a PID to obtain a percentage of gate opening. According to emergency stopping informations, the unit decides then if it takes the gate under control, and updates the logical informations concerning the switching of the protection system.
On the other hand, the unit computes the nuclear power as a function of the steam pressure (tabulated function).
The unit is classified as a safety critical device: it is only active during an emergency stopping. Its validation is considered to be critical in the development process.
It has been developed using the tool Saga. It is made of about 40 Lustre nodes, and 7 functions in C. Schneider-Electric will provide
- the requirement document of the unit
- the description of the unit, either in Saga or in Lustre
- a set of safety properties to be verified
- properties to help the generation of test sequences
- any assistance needed to understand the case.
SAAB-MA proposes to use the air control system in aircraft JAS 39 for a case study. The system supports different ``users'' in the aircraft, for example the pilot and the cockpit with tempered air and the cooling of the electronics. The system is an integrated system of hardware --- like valves to regulate the air flow and switches to indicate valve positions --- and software, which controls the movement of all hardware to produce the right amount of tempered air flow.
In case of degradation, resulting in that the air system cannot fulfill all the ``users'' needs, automatically the ``users'' will be served according to some priority ordering. This automatic coupling down of the system is very important and can be safety critical if performed wrongly.
Today there is a model of the system in ASA.
Back to the Proposal ToC
Steam Generator Water Level Control System
This case study is proposed by EDF.
Steam Generator Water Level Control System
Steam generators in PWR's ensure the cooling of the reactor and provide steam to the turbine. The feedwater system has to keep the mass balance on the secondary side of the steam generators. To fulfill this function, the operator has to maintain the water level in steam generator downcomer close to its setpoint by means of the feedwater control valves.
Steam generator (SG) water level control system operates over the entire power range and ensures:
- the automatic control of the steam generator water level,
- control operations during normal or fault modes: start-up, automatic/manual, failures, emergency/protection, ...
- alarms synthesis
- user interface and user operations management.
Many signals are used in the control of a SG control, like : Feedwater Flow, steam flow, Feedwater Temperature, Turbine Load, Narrow Range Level, Wide Range Level, Operation Mode Selection, Steam Header pressure, Feedwater Header Pressure, Valves positions, High Level Alarm, Low Level Alarm, ...
Analogic and logic functions are involved in the control, such as :
- valves positions controller,
- Steam Generator water level controller,
- Feedwater/Steam difference pressure controller,
- Feedwater pump speed controller,
- controllers switching,
- signal validation of sensors,
- failure detection of equipments,
- valves sequencing logic,
- normal and fault operation modes logic,
- user operations sequencing,
- pumps switching logic,
- alarms synthesis,
- protections.
Verification and validation of some critical properties of this control system are important for operations and safety. For example, some operating difficulties during start-up or when faults occur are the frequent cause of unexpected tripping of the reactor or turbine.
EDF/DER will provide a derived case study of the Steam Generator Water Level Control System including requirements and specifications of:
- a simplified steam generator physical model,
- a steam generator water level controller and other controllers needed for the level control,
- logic functions needed for alarms synthesis, operations sequencing, protections, switching, ...
- a set of operations and logical safety properties to be verified,
- assistance needed to understand the case.
One of the important features of this study case is the steam generator physical model representation; hybrid validation methodology has to be considered.
We detail now, for each research area, the available results and the projected work.
Background.
Available synchronous formalisms are, on one hand, either graphical or textual, and, on the other hand, either imperative or declarative (data-flow). The differences in style and focus reflect different objectives. While for instance the imperative style more addresses the construction of discrete controllers, the declarative style more supports ``continuous'' change of state such as in sensor/actuator systems or digital signal processing.
Experience shows that the existence of several synchronous formalisms is more an advantage than a drawback: these formalisms appear to be complementary, as some applications, or even some parts of applications, are easier to specify in some formalism. As a consequence, there is a strong need to combine these languages together, so as to allow the user to freely merge the various points of view. For instance, a discrete change of state may be needed for a sensor/actuator system in order to model major changes of mode of operation. Rather than to model such a change of state by some boolean flags, a combination of a state-based language such as Argos with some declarative language such as Lustre or Signal will provide a smooth and lucid programming style in that the states of Argos correspond to modes of operation while refinements of these states by declarative programs determine the actual operation. On the other hand Esterel would be best suited for modelling control tasks which are mainly interrupt driven.
It is as well often convenient to write programs in one language and an observer for testing and verification (see Section on verification ) in another language, or to use different languages for hardware description, e.g., Esterel is better suited for modelling control while the declarative languages are better suited for modelling digital signal processing (DSP).
Production compilers and development environments are already marketed by software companies for the imperative synchronous programming language Esterel and the declarative synchronous programming languages Lustre and Signal. The graphical, state-based synchronous language Argos will be supported by a graphical editor developed at GMD, a prototype of which is available.
The designers of the three languages Esterel, Lustre, and Signal, have cooperated for several years in defining internal formats for the interchange of whole programs between tools. For the combination of formalisms, however, a semantical framework is needed for the integration of programs at the level of object code.
At GMD, a combination of Argos and Lustre has already been implemented which allows arbitrary Lustre modules to be imported for refinement of Argos states, thus enabling discrete change of mode on top of (discrete time) continuous state models. The integration is based on a proprietary internal format (which roughly is an enhancement of the internal formats developed in ``SYNCHRON''), and on a common paradigm for compilation of the languages involved (a compiler based on the same paradigm is as well available for pure Esterel). The format supports linking of arbitrary modules which are presented in the internal format. So far, the combination has been achieved only for the ``pure'' part of the languages, i.e., the only data types supported are signals and booleans, and integration is restricted to the behavioural aspect, meaning that, so far, a deeper analysis of a combination of clock checking mechanisms --- as in Lustre and Signal --- and causality analysis --- as necessary for Argos and Esterel--- is still missing.
As compared to an exchange via common formats, the integration envisaged is seamless, meaning that every module may be freely imported to and exported from any of the supported synchronous languages.
It should be mentioned that another such combination is provided by the commercial environment Statemate where the (state-based) Statecharts are complemented by the (data-flow based) Activity-Charts although with no work on formal semantics and uniform verification framework. Another example of related work is an attempt [see `` C. Petersohn, C. Huizing and J. Paleska. A Comparison of Ward &Mellor's Transformation Schema with State- and Activity Charts. Technical Report 94/11, Eindhoven University of Technology, 1993.'' ] to defining a formal semantics for Ward-Mellor structured design languages, which also have both imperative (control-oriented) parts and declarative (data flow) parts. However, these approaches either lack the tight and clean semantically-based integration or they are not yet in a status where industrial exploitation can be envisaged
The synchronous formalisms as promoted by the present research proposal, have the unique feature of being based on a semantically sound uniform paradigm, which supports a tight combination of the different styles on different levels of abstractions, as demonstrated by prototypical implementation, and, last not least, of being industrially viable.
Proposed research.
A tight integration of synchronous formalisms will need further research on the following topics, which are closely related:
- Up to now, the formal semantics of synchronous languages is
presented rather different in style, ranging from structural
operational semantics to data-flow based denotational semantics.
Hence proofs of correctness of compilation schemes are restricted to
the respective language and its specific style of semantics.
Quite clearly, neither these compilation schemes nor the respective proofs are prepared for the import of modules that stem from other languages. Thus the schemes have to be relativised with regard to imports from other paradigms, and a common semantical framework has to be set up.
Then the original correctness proofs have to be re-established with regard to this framework in such a way that correctness is independent of the nature of imported modules. The technique is to use invariants for characterisation of imported modules and then to show that the translation schemes are correct relative to these invariant. This techniques has been implicitly used in [53] where invariants are used as lemmas.
- The tight integration, as sketched above, relies on particular
assumptions with regard to the compilation schemes. Given that an
integration is achieved on this basis, there is still the question
whether the present industrial strength compilers can be adapted to
support a seamless combination of formalisms, and if so, to modify
these compilers respectively.
- In addition, algorithms for causality analysis and clock
analysis have to be adapted and relativised to the combined
formalisms. Apart from the general difficulty of finding such
algorithms, particular attention has to be paid to designing
algorithms which are as well liberal in accepting ``reasonable''
programs as they provide succinct feedback to the programmer why a
program is rejected or accepted.
More particularly, it seems to be fairly simple to localise clock-checking: clock correctness of a module (or a cluster of modules within one language) can be checked on its own, by assuming that outputs of imported modules behave as inputs, either being unconstrained or constrained (in the latter case there is the obligation to check whether an imported module satisfies the constraints). In contrast, there is little hope to modularise causality analysis even though the declarative languages avoid causal loops by syntactic means (no recursive use of a variable except if memorised).
Finally, the ideas and the benefits of the approach will be demonstrated by a major industrial case study provided by the industrial partners.
- deliverable 2.1 (12 months)
- : Definition of the translation
schemes plus correctness proofs, first prototypical implementations
of the combined formalisms as sketched above, setting up the
supporting tools for the workbench
- deliverable 2.2 (24 months)
- : Refinement of the schemes with
regard to efficiency of translation, algorithm for causality analysis
and clock checking defined, stabilising the compilers, and completing
the workbench, preparation of the case study, check whether results
transfer to industrial strength compilers
- deliverable 2.3 (36 months)
- : application of the workbench to
the case study
Back to the Proposal ToC
Program Verification and Validation
Concerning program verification, the synchronous approach has several
advantages. Verification on finite-state models (model-checking,
automata abstraction) is more successful, because considered models
are smaller. Moreover, synchronous languages offer an original way
for specifying critical properties, by means of synchronous
observers [30]. This makes formal verification tools easily
accessible to engineers, as shown by several realistic industrial
experiences (e.g., [35]).
However, because of the intrinsic
difficulties of the subject (complexity, undecidab
ility), the
verification techniques must be investigated furth
er. We strongly
believe that the various approaches should be cons
idered complementary,
rather than competing. So many different approache
s will be studied,
with the concern of combinating them together:
Program Verification and Validation
- Concerning finite-state systems, both BDD techniques (Section [->]) and tautology checkers (Section [->]) will be studied and compared.
- Concerning infinite state systems, both approximate techniques (Section [->]) and theorem proving (Sections [->] and [->]) will be investigated, and possibly integrated with finite-state techniques.
- For problems which are outside the range of formal verification, only testing methods can be applied; they can benefit from verification techniques (Section [->])
Background.
Boolean equation systems form a natural intermediate model of synchronous formalisms: they bear close ties to hardware circuits at the gate-register level; they exhibit natural synchronous parallelism; they provide means to describe the Mealy finite state machines (FSMs) transitional behaviours. This is why this level has been chosen for the common format DC/DC+. What boolean equations do not provide is the actual space of reachable configurations. While the synchronicity assumption disfavours size blow-up, this state space can still become unmanageably large in real cases. Boolean encoding of sets of states (as in BDD-based tools, or in methods using tautology checkers) have been recently largely successful in coping with state explosion by implicit/symbolic representation. Further analysis techniques have been reduced to methods very similar to symbolic state space computation, and including it. The scope is here to provide powerful means of analysis to the user without requiring much theoretical expertise from him.
Proposed research.
We shall explore further promising steps in the following directions:- Abstraction by reduction of FSMs at symbolic level. By
abstracting away signals from the interface when irrelevant for the
current analysis, one may produce substantially smaller FSMs, which
can be submitted to further model-checking, or simply observed by
humans for correctness check. An interesting typical case is when,
from a hierarchical description, a given subcomponent is compared to
the global system abstracted back to its interface. One then gets a
measure of disturbance in interactions with the rest of the system.
- Compositional reductions of boolean equation systems. By this
means, behaviourally identical but smaller descriptions could be
substituted in place for subcomponents at this level. This activity
will be conducted in close relation with work on combination of
formalisms, since the syntactic program structure should help in
defining the blocks on which to apply compositional minimisation.
- Easy formulation of particular sets for model-checking. Most properties of interest on reactive systems can be phrased as safety formulae (a given particular set of configurations cannot be reached) or liveness formulae (it is impossible to loop forever across particular behaviours, without eventually reaching a given particular set of configurations). While model-checking is now well understood algorithmically, at least on pure control parts of systems, it still requires expertise to specify the basic particular sets (of states, of transitions) as predicates on the system. This is usually done at the intermediate level of distributed FSMs, and needs awareness of this level from the user. In the case of synchronous reactive systems there exist nice formal ways of extracting these predicates at original language level, such as synchronous observers, or program instrumentation by additional witness output signals. We need to make these easily available to the regular program developer, so that program transformations remain internal and transparent, while powerful description is allowed.
- deliverable 3.1.1 (12 months)
- : Prototype tool on abstraction and FSM minimisation distributed to partners.
- deliverable 3.1.2 (24 months)
- : Prototype tool on compositional simplification of boolean equation systems distributed to partners. Prototype tool on ``easy'' specification of particular sets for model-checking. Case studies on abstraction and feedback.
- deliverable 3.1.3 (36 months)
- : Case studies on compositional
simplification of boolean equation systems. Final tool versions.
Background.
The use of automated formal verification tools is preferred since it lets system developers focus on requirement specification and design rather than more or less elaborate verification procedures, requiring a lot of manual assistance and expert knowledge. Such tools cannot be developed without efficient theorem proving techniques. Binary Decision Diagrams, BDDs, are by many considered the best approach. However, in many applications, the Stalmarck method [60] is a strong competitor to BDDs. E.g., in a recent investigation [see ``J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd. Technical report, Department of Philosophy -- Utrecht University, 1994.''] , the method even proved superior. Up to date the performance of the Stalmarck method is sufficient for some applications, but not all [E.g., when large arithmetic domains are used.] ; consequently the verification procedure needs to be improved.
It has already been shown that the efficiency of the method allows for implementation of fully automatic, industrial verification tools [57]. The method is based on the following results:
- (finite) systems can be represented in propositional logic extended with finite domain constraints
- (most) such systems can be verified using a tautology checker
- verifiable systems have short proofs
- the Stalmarck method will find short proofs fast.
The method allows the use of propositional logic extended with finite domain constraints. This feature simplifies representation of both requirements and systems. However, right now there is a penalty in efficiency when large domains are used. In order to cope with this, hybrid techniques have evolved, combining the Stalmarck method with finite domain constraint solving [19], originating from the idea of indexicals [18]. The preliminary results are promising. However, other approaches may need to be considered as well (see Section [->]).
Since 1995, Volvo has been using synchronous methods in a project together with Logikkonsult NP AB, aiming at producing verifiable specifications, by developing them in SAO+, and verifying them using NP-Tools[A verification tool based on the Stalmarck method]. Preliminary results show that lack of methodology, not efficiency, is the bottleneck regarding application of the Stalmarck method in synchronous systems development. Support for representing mixed synchronous/asynchronous systems also needs to be developed, including methodology.
Proposed research.
-
Representing (a)synchronous systems in formalisms suitable for
automatic verification using the Stalmarck method. This research
will be based on on-going work within project SYNCHRON.
-
Expressing (safety) properties of (a)synchronous systems in formalism
suitable for automatic verification using the Stalmarck method.
This research will be based on on-going work within project
SYNCHRON.
-
Proving (safety) properties of (a)synchronous systems using theorem
proving techniques that combine the Stalmarck method with
constraint solving techniques. This work will be based on on-going
research within the Swedish competence center ASTEC
[A Swedish competence center sponsored by Swedish industry
and the Swedish National Board for Technical Development.].
-
Proving (safety) properties of (a)synchronous data-flow systems using
the Stalmarck method (Section [->]).
-
Improving the handling of arithmetic (see Section [->])
constraints in the Stalmarck method.
-
Comparing state-of-the-art verification techniques, by means of the
results of program verification applied on the cases in the
project (see Section [<-]).
-
Generating test patterns using the Stalmarck method (Section
[->]). This research will be based on work performed in
telecommunication applications (with Ericsson), but that need to be
further developed.
- deliverable 3.2.1 (12 months)
- :
- Developing an interface to the workbench in NP-Tools
(Proposition 1).
- Support for expressing properties and requirements in
synchronous systems (Proposition 2).
- Improving the Stalmarck method for analysis of synchronous
systems (Proposition 5, Sections [<-]
and [->])
.
- System verification of supplied cases (Proposition 4).
- Developing an interface to the workbench in NP-Tools
(Proposition 1).
- deliverable 3.2.2 (24 months)
- :
- deliverable 3.2.3 (36 months)
- :
- Support for automatic generation of test patterns for
synchronous systems using the Stalmarck method (Proposition 7).
- Evaluation report.
- Support for automatic generation of test patterns for
synchronous systems using the Stalmarck method (Proposition 7).
Back to the Proposal ToC
Handling Properties Depending on the Behaviour of
Numerical Variables
Handling Properties Depending on the Behaviour of
Numerical Variables
Background.
Any synchronous program can be viewed as an interpreted automaton, i.e., a finite control structure, the transitions of which are augmented with conditions and actions on variables. Existing verification tools for synchronous programs are based on the control structure, and ignore the interpretation. This abstraction has been shown to be reasonable in many practical cases, since the critical properties of a reactive system often depend only on the control. However, there are cases where the behaviour of datas must be taken into account.Using the technique of synchronous observers, any safety property of a synchronous program can be expressed as the unreachability of some states in the interpreted automaton. Finite-state-based methods, which generally abstract away the interpretation, sometime wrongly conclude that these ``bad'' states can be reached. Two approaches are proposed to obtain more precise results:
- A static method, whose goal is to cut, in the automaton, transitions that are guarded by unfeasible conditions. Interesting results can be obtained using a procedure checking the satisfiability of systems of linear constraints. This method has been incorporated in Lesar, a tool developed at INRIA/Spectre for the verification of Lustre programs (actually working on DC format), and gave satisfactory results on a real example at Schneider-Electric [35].
- A more ambitious dynamic method, taking into account the dynamic behaviour of numerical variables. Based on abstract interpretation, this approximate method gives quite precise results, in particular for properties involving real-time delays [31]. The analysis tool Polka, also developed at INRIA/Spectre, is based on this method, and is currently one of the most powerful, fully automatic verification tool taking unbounded numerical variables into account.
Proposed research.
Several experiments on real-life case studies showed that the main limitation of these methods is not due to the result imprecision, but rather to problems of performances: both approaches are based on an explicit representation of the control automaton, the size of which is often prohibitive.As a consequence, we propose to study a combination of these numerical methods with an implicit representation of the control structure, by means of BDDs. A possible track consists in starting from a rough control structure, which would be progressively refined in a demand-driven way. A mixed representation, merging Boolean and numerical aspects, will probably have to be defined.
Based on real case studies, this work will result in a prototype verification tool.
- deliverable 3.3.1 (12 months)
- : Detailed description of the method.
- deliverable 3.3.2 (24 months)
- : Prototype verification tool.
- deliverable 3.3.3 (36 months)
- : Experiment report and tool documentation.
Back to the Proposal ToC
Deductive Proofs of Data-flow Programs
Deductive Proofs of Data-flow Programs
Background.
Recently, several toolboxes for program formal derivation and proof have been proposed, among which we can cite B [see ``J.-R. Abrial. The B-Book. Cambridge University Press, 1995.'' ] , VDM [see ``C. B. Jones. Systematic Software Development using VDM. Prentice Hall International, 1990.'' ] , Z [see ``J.M. Spivey. Understanding Z: A specification language and its formal semantics. Cambridge University Press, 1988.'' ] , Coq [see ``T. Coquand and G. Huet. The calculus of construction. Information and Computation, 76(2), 1988.'' ] , and PVS [see ``S. Owre, J. Rushby, and N. Shankar. PVS: a prototype verification system. In 11th Conf. on Automated Deduction, LNCS 607, Springer Verlag, 1992.'' ] . Clearly this growing interest is due to the also growing involvement of software in critical systems, and the consequent concern about software errors.
These critical systems can arise from many fields, but one field which yields some of the most critical ones is the field of automatic control and monitoring systems; this can be easily illustrated by examples drawn from civil aircraft, nuclear plants and automatic ground transportation systems.
In these domains, synchronous data-flow programming has become a popular approach, for the quite obvious reason that automatic control engineers use to analyze and specify their systems in terms of signals flowing through networks of operators (block diagrams). Thus synchronous data-flow languages allow them to directly translate their specifications into code without undertaking a manual, error-prone coding phase. Several real-world achievements have been obtained in this way, among which we can cite the ``fly-by-wire'' system of Airbus aircrafts, the monitoring system of Framatome nuclear plants, designed by Schneider Electric, and the interlocking system of the Hong Kong subway designed by CS-Transport. Of these examples, the last two have been based on the Lustre data-flow synchronous language [28].
This has entailed a need for formal methods adapted to this language. A long lasting effort has already been made in this direction, mostly based on ``model checking'' techniques [29]. Model-checking was a good choice since automatic control programs have a control structure consisting of a finite automaton, over which most properties are decidable. Moreover, even properties involving unbounded data types, like integers or reals can be decidable. This is the case of linear (integer) programming problems for instance (see Section [<-]).
Yet there are many control problems which don't fall into such class, and should be handled within more general deductive frameworks like the ones cited above. Typical examples can be found in automatic railway systems where control systems have to deal with Newtonian dynamics, for instance.
Proposed research.
The goal of the action is to investigate the application of the PVS approach to Lustre programs. The choice of PVS is motivated here because it is a well-equipped and freely available tool. Yet, this is not to preclude other approaches and on the contrary, it can be expected that the lessons drawn from this research will serve in other frameworks. We propose to proceed stepwisely as follows:
- The first task will consist in expressing Lustre problems in PVS
terms. One issue here is to cope with feedback loops in data-flow
diagrams, which could be naturally translated by recursion,
notwithstanding the fact that recursion over infinite sequences is not
allowed in PVS. Several solutions to this problem exist and we shall
compare them from both points of view of user-friendliness and
efficiency.
- This will allow us to handle several case studies. We shall try to
select them from several domains and concentrate on cases where
model-checking doesn't apply, in order to emphasise the complementary
aspects of both methods.
- Finally, we shall study and prototype a front-end allowing to handle the
translation automatically, thus making the approach a practical one.
- deliverable 3.4.1 (12 months)
- : Comparative study of data-flow to
PVS translations.
- deliverable 3.4.2 (24 months)
- : Case studies on checking data-flow
programs with PVS.
- deliverable 3.4.3 (36 months)
- : Front-end prototype.
Back to the Proposal ToC
Use of Automata Technology and Synchronous Observers for
Automatic Testing
Automatic help in program testing is an important demand from
industrial users. We propose to adapt and extend for this purpose the
technology developed for synchronous program verification:
Use of Automata Technology and Synchronous Observers for
Automatic Testing
- On one hand, synchronous observers can be used to express
- the expected behaviour of the program under test;
- the constraints assumed about the behaviour of the environment;
- the testing objective.
- On the other hand, automata-based techniques can be applied to
synthesise test sequences satisfying both the environment constraints
and the test objective. The result is an interpreted automaton
deciding, in each of its states, which test cases can be chosen.
- Finally, instead of randomly chosing test cases before
submitting them to the automaton (considered as an acceptor),
it would be much better to transform the automaton into a generator. Symbolic techniques based on BDDs and polyhedra (for
numerical variables) can be applied for that.
- deliverable 3.5.1 (12 months)
- : External specification of the tester. Study of main internal algorithms.
- deliverable 3.5.2 (24 months)
- : Prototype implementation of the tester.
- deliverable 3.5.3 (36 months)
- : Experiment report and tool documentation.
Back to the Proposal ToC
Code distribution and Multi-Tasking
Code distribution and Multi-Tasking
Background.
At the implementation level, available industrial compilers only produce standard sequential code. Other implementations must be studied, concerning distributed code generation, and integration with real-time operating systems offering multitasking and some kind of asynchrony.A large part of the process of code generation based on synchronous technology is independent of target architecture. Unique features of synchronous technology for this purpose are available in the Signal language and the DC/DC+ common formats, they are listed now:
- Possibility to abstract the communication interface of a module
in the form equivalent to an automaton --- this is already classical
in the stepwise refinement approaches.
- The following feature, however, is unique to synchronous
techniques. A primitive, we denote it by ``depends'', allows
state-dependent scheduling constraints to be specified.
More precisely, ``Y depends X when COND'' expresses that the
flow Y cannot be produced before flow X when COND
is satisfied. This can be used to describe causality constraints, or
alternatively, for specifying additional scheduling constraints that
one may want to impose on the different actions. This is also useful
to abstract a program to its interface, by summarising both the
communication automaton and the scheduling of the communications.
- The functional architecture of the application at different levels of detail.
- The target architecture for implementation, based on synchronous model.
- A profiling of (1) as mapped onto (2), i.e., a model of real-time behaviour of this mapping. This model can then be used for timeliness simulations or for timeliness formal verifications.
Proposed research.
A further step will consist in developing a next layer below the low level description of target architecture following synchronous model. This layer will have the form of a nano-kernel OS composed of a small library of real-time primitives, called Real-Time Library (RTL). RTL will satisfy the following requirements:- It should allow to control properties of the design all the way down from target architecture description following synchronous model down to RTL description.
- It should allow to confront the predictions based on profiling to reality via simulations.
- It should allow to emulate typical real-time kernels actually used in real-time designs.
- deliverable 4.1 (12 months)
- : detailed specification of RTL,
and of profiling techniques.
- deliverable 4.2 (24 months)
- : prototype RTL, comparisons of
profiling predictions with RTL simulations.
- deliverable 4.3 (36 months)
- : experimentation on test case;
limited release according to robustness of the prototype tool.
Back to the Proposal ToC
Integrating Synchrony and Asynchrony
Synchronous programming only solves a part of the problems raised
by the design of a complex real-time systems. In general, synchronous
programs must be integrated in a complex, asynchronous environment.
There is a strong need for models integrating synchronous and
asynchronous features, while offering a global view of the system,
preserving a clean formal semantics, and allowing formal verification at
the global level. The language CRP [12], which combines
Esterel and CSP, is an attempt in that direction.
Integrating Synchrony and Asynchrony
Back to the Proposal ToC
Automatic Verification on Mixed A/S Systems
Our goal here will be to deal with specifications consisting of asynchronous networks of synchronous systems, where ``asynchrony''
here refers to processes evolving at a different pace, and
synchronising by mutual rendez-vous (such as in CCS, CSP or Lotos
languages). Individual sequential components will now become whole
synchronous programs, at synchronous sites, while asynchronous
networks form an extra level where the synchronicity assumption
cannot be assumed anymore. As an example telecommunication
protocols consist of end-processes such as emitters/receivers or
servers/clients, each of which is a synchronous system with
increasing complexity, but whose correctness can only be asserted
when modeling the asynchronous network media. In our opinion, many
concurrent systems can adequately be represented as programmed
synchronous parts communicating across specified asynchronous
networks.
Automatic Verification on Mixed A/S Systems
Model-based analysis is a well-developed topic both for synchronous and asynchronous systems of processes, independently. It is made possible by formal semantics, and relies heavily on FSM interpretation and reachable state space construction. Many useful verifications can then be conducted by encoding properties as observers and dealing with a product machine.
Symbolic techniques, and in particular BDDs, are now the prominent implementation method for (symbolic) state space representation and exploration. Still, algorithmic efficiency on such data structures demands that the transition relation representation be optimised, by partitioning. There the synchronous and asynchronous domains each lead to distinct partioning schemes : In synchronous programs, a state consists of a vector of state variables, each of which is a function of the previous state and input (determinism); so, partitioning consists of representing the transition relation as a vector of (small) functions. In asynchronous process algebras, each global transition only involves a small number of processes; so the transition relation can be represented as a union of (simple) relations.
We shall provide a description formalism for such mixed systems (at specification level), and study further the integration of actual efficient BDD-based tools for either synchronous or asynchronous systems in a unified framework. There external synchronisation offers must be included in a synchronous FSM model in a way compatible with transition relation partitioning.
- deliverable 5.1.1 (12 months)
-
Definition of a programming/specification language (probably as a
superset of Esterel) for mixed A/S systems, and early prototype tool
for model-based analysis.
- deliverable 5.1.2 (24 months)
-
Experiments on case studies (protocols,...) and development of a
stable version. Distribution to project partners.
- deliverable 5.1.3 (36 months)
- Documentation and public release.
Back to the Proposal ToC
From Strong Synchrony to True Concurrency, and Back
Work on both the DC/DC+ common formats for synchronous
languages, and on the Signal language have resulted in the
introduction of a specific primitive related to scheduling
constraints. This primitive, we denote it by ``depends'',
allows to specify a state-dependent scheduling constraint (see
Section [<-]). More precisely, ``Y depends X when
COND'' expresses that flow Y cannot be produced before flow
X when COND is satisfied. This can be used to describe
causality constraints, or alternatively, for specifying additional
scheduling constraints that one may want to impose on the different
actions. This is also useful to abstract a program to its interface,
by summarising both the communication automaton and the scheduling of
the communications.
From Strong Synchrony to True Concurrency, and Back