PAFESD

Process Algebras for Electronic System Designs (PAFESD)

During the last few years, the use of formal languages has become more and more clear as a prominent approach to specify various systems (e.g. real-time and hybrid systems). Also, several flavours of formal languages have gained industrial acceptance.

Process algebras are formal languages that have formal syntax and semantics for specifying and reasoning about different systems. They are also useful tools for verification of various systems. Generally speaking, process algebras describe the behaviour of processes and provide operations that allow to compose systems in order to obtain more complex systems.

Moreover, the analysis and verification of systems described using process algebras can be partially or completely carried out by mathematical proofs using equational theory.

Recently, through novel language constructs and well-defined formal semantics, several hybrid process algebras (Hybrid Chi, HyPA, ACP^srt_hs and BHPC) and timed process algebras (Timed Chi and mCRL2) have been developed. They can be reasonably and effectively used to give formal specifications of analog/mixed-signal (AMS) and hardware system designs.

In addition to the traditional simulation analysis of such designs, various sophisticated analysis approaches or techniques (e.g. algebraic reasoning, formal verification and linearisation algorithms) can be applied to such designs described in process algebra based formalisms.

In the frame of a tight collaboration between researchers from industrial entities and the research institute CEOL (the Centre for Efficiency-Oriented Languages), our applied research in this direction is to use the above-mentioned process algebras to address various aspects (e.g. formal specification and analysis) of industrial analog/mixed-signal and hardware system designs.

The research activity of PAFESD is partnered with

For questions, suggestions and comments, please send mail to Pafesd@gmail.com