Formal Analysis of Heterogeneous Embedded Systems using Tagged Signal Models

by

Soumyajit Dey

Supervisors: Prof. Anupam Basu and Prof. Dipankar Sarkar

The design of complex and heterogeneous embedded systems frequently requires different models of computations (MoCs) for modeling different sub-systems. In these cases, there is a need for a heterogeneous behavioral modeling technique that makes it possible to reason formally on the combination of these models, i.e., their “product”. The denotational framework of tagged signal models (TSM) has long been advocated as a unified modeling framework that can capture the essential features of different MoCs. A tagged signal model defines precisely processes, signals, events and provides a framework for capturing the essential properties of MoCs like discrete-event models, dataflow models, rendezvous-based systems and process networks.

In the present work we embark on a two-fold objective. One is to evaluate the performance of heterogeneous designs, given an execution policy, using the model of tagged systems as an intermediate representation. The second one is to provide an algebraic characterization of the tagged systems by showing its conformance to the structure of Kleene semirings. Such a characterization helps in equational reasoning on heterogeneous specifications using the axioms of Kleene algebra.

The denotational semantics of tagged systems deals with behaviors captured by ``traces'' which is not a finite model of the underlying system. The theory of tag machines has recently been proposed as a finitary representation framework of the tagged systems. Tag machines are able to capture a wide range of concurrency models like asynchronous, synchronous-reactive, Time Triggered Architectures (TTA) and causality. The framework of tagged systems is based on the concept of tags. A tag structure represents an ordering relationship among events, sequences of which describe the system behaviors. Depending on the choice of the tag structure, a tag machine can capture a given concurrency model. However, such machines are not natural representations of system specifications which is possible using formalisms like Kahn Process Network (KPN), Timed Automata (TA), Synchronous Dataflow Graphs (SDFG), etc. Hence, an immediate requirement becomes formulating translation mechanisms from such specification models to tagged representations which can be composed. In this front, we have devised such a methodology for translating a given TA model to a tag machine. As a case study, we took jobshop schedules given as TAs and derived corresponding tag machines. Using the resulting compositional machine, we could derive the asymptotic throughput of an infinite jobshop schedule which was not possible using the corresponding TA representation. Apart from TA, we have also shown the applicability of our approach to asymptotic performance evaluation of systems modeled using SDFGs. Further, we have verified the applicability of our approach in case of heterogeneous systems by evaluating the performance of a system comprising of dataflow and discrete-event blocks.

In order to provide an algebraic characterization of tagged systems, the second part of the work builds on domain theory, developed for the denotational semantics of programming languages. Actor oriented formalisms established in the last two decades are based on such concepts. Similarly, in the tagged signal model, we have the concepts of actors mapping a set of input signals to a set of output signals. In the original model of tagged signals (popularly known as LSV named after Lee and Vincentelli), the set of all such tagged signals has been shown to form a complete partial order (CPO). We show that a similar result can be derived in the context of the more succinct version of the model which is proposed in [1]. Our actors support bounded, value-based, biased non-determinism. We further prove that the set of all such possible TSM actors is closed under the axioms of Kleene algebra (KA) and its extensions like Kleene algebra with Test (KAT) and Kleene Algebra with Domain (KAD) [2]. The result has important consequences. For a given a heterogeneous system specification, we can transform it into a corresponding TSM actor based representation which can be encoded as an algebraic expression of KA/KAT/KAD. Using the axioms of these algebras, we can perform property verification as well as functional equivalence checking of such complex systems. As a case study focussed on equivalence checking of heterogeneous embedded systems, we construct two different implementations of a Reflex Game modeled using the Synchronous Reactive (SR) MoC, derive the corresponding KAT based encodings and prove their equivalence.

Further, we provide a TSM based model of the European Train Control System (ETCS) protocol and perform the safety property verification by applying KAT rules over the Kleene expressions of the actor network.

References

[1] A. Benveniste, B. Caillaud, L. Carloni, P. Caspi and A. Sangiovanni-Vincentelli, “Composing Heterogeneous Reactive systems”, ACM Trans. Embedded Computing Systems, Vol. 7, No. 4, pp 1-36, 2008.

[2] Dexter Kozen, “Kleene algebra with tests”, ACM Trans. Programming Languages and Systems, Vol. 19, No. 3, pp. 427-443, 1997.