Interoperability of Performance and Functional Analysis for Electronic System Designs in Behavioural Hybrid Process Calculus (BHPC)

  • Ka Lok Man
  • Michel P. Schellekens
Part of the Lecture Notes in Electrical Engineering book series (LNEE, volume 6)

Hybrid systems are systems that exhibit discrete and continuous behaviour. Such systems have proved fruitful in a great diversity of engineering application areas including air-traffic control, automated manufacturing, and chemical process control. Also, hybrid systems have proven to be useful and powerful representations for designs at various levels of abstraction (e.g., system-level designs and electronic system designs.

In this chapter, we aim to show that it is reasonably easy to translate the half-wave rectifier circuit described in BHPC to the input languages of the above-mentioned tools and to analyse them in those environments. Hence, general translation schemes from BHPC to other formalisms (i.e., input languages of the OpenModelica system and the model checker PHAVer) are briefly described. However, for brevity, translations presented in this chapter between BHPC and other formalisms are not studied and discussed at the semantic level (to ensure that interesting properties can be preserved by the translations). Nevertheless, it is worth mentioning that the translation from BHPC to the input language of the OpenModelica system and from BHPC to the input language of PHAVer could already be automated (see Sect. 27.6 for details).

This chapter is set up as follows. Section 27.2 provides a brief overview of the behavioural hybrid process calculus (BHPC). A sample (modelling a half-wave rectifier circuit) of the application of BHPC is shown in Sect. 27.3. Section 27.4 first briefly presents the tool OpenModelica system and its input languages, the Modelica language [15]; and then shows how to do performance analysis on the half-wave rectifier circuit described in BHPC using the OpenModelica system. Similarly, Sect. 27.5 first gives a brief summary of the model checker PHAVer and its input language: the theory of hybrid I/O-automata [16]; and then illustrates how to perform functional analysis on the half-wave rectifier circuit described in BHPC using PHAVer. Related works are given in Sect. 27.6. Finally, concluding remarks and future works can be found in Sect. 27.7.


Hybrid System Process Algebra Hybrid Automaton Input Language Continuous Behaviour 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baeten, J.C.M., Weijland, W.P.: Process Algebra. Volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK (1990).Google Scholar
  2. 2.
    Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. EACTS Monographs in Theoretical Computer Science. Springer-Verlag, New York (2002).MATHGoogle Scholar
  3. 3.
    Man, K.L., Schiffelers, R.R.H.: Formal specification and analysis of hybrid systems. PhD thesis, Eindhoven University of Technology (2006).Google Scholar
  4. 4.
    Cuijpers, P.J.L.: Hybrid process algebra. PhD thesis, Eindhoven University of Technology (2004).Google Scholar
  5. 5.
    Bergstra, J.A., Middelburg, C.A.: Process algebra for hybrid systems. Theoretical Computer Science 335(2/3) (2005) 215–280.MATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Krilavičius, T.: Hybrid techniques for hybrid systems. PhD thesis, University of Twente (2006).Google Scholar
  7. 7.
    Plotkin, G.D.: A structural approach to operational semantics. Technical Report DIAMI FN-19, Computer Science Department, Aarhus University (1981).Google Scholar
  8. 8.
    van Beek, D.A., Man, K.L., Reniers, M.A., Rooda, J.E., Schiffelers, R.R.H.: Syntax and consistent equation semantics of hybrid Chi. Journal of Logic and Algebraic Programming 68(1–2) (2006) 129–210.MATHMathSciNetGoogle Scholar
  9. 9.
    Rounds, W.C., Song, H.: The ϕ-calculus—A hybrid extension of the π-calculus to embedded systems. Technical Report CSE 458-02, University of Michigan, USA (2002).Google Scholar
  10. 10.
    Man, K.L., Reniers, M.A., Cuijpers, P.J.L.: Case studies in the hybrid process algebra hypa. International Journal of Software Engineering and Knowledge Engineering 15(2) (2005) 299–305.CrossRefGoogle Scholar
  11. 11.
    Man, K.L., Schellekens, M.P.: Analysis of a mixed-signal circuit in hybrid process algebra \text{ACP}hs srt. In International MultiConference of Engineers and Computer Scientists, Hong Kong (2007).Google Scholar
  12. 12.
    Krilavi\breve{\text{c}}ius, T.: Study of tools interoperability. Technical Report TR-CTIT-07-01, University of Twente, The Netherlands (2007).Google Scholar
  13. 13.
    OpenModelica System Web site: Openmodelica system
  14. 14.
    Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In Morari, M., Thiele, L., eds.: Hybrid Systems: Computation and Control, 8th International Workshop. 3414, LNCS. Springer-Verlag, New York (2005) 258–273.Google Scholar
  15. 15.
    Modelica Association: Modelica — A unified object-oriented language for physical systems modeling, (2002).
  16. 16.
    Lynch, N., Segala, R., Vaandrager, F.: Hybrid I/O automata. Information and Computation 185 (1) (2003) 105–157.MATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Carloni, L.P., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.L.: Language and tools for hybrid systems design. Journal of Foundation and Trends 1 (2005) 1–177.Google Scholar
  18. 18.
    Frehse, G.: Language overview v. for PHAVer v.0.2.2, (2004).
  19. 19.
    Khadim, U.: A comparative study of process algebras for hybrid systems. Technical Report CS-Report 06-23, Eindhoven University of Technology, The Netherlands (2006).Google Scholar
  20. 20.
    van de Brand, P., Reniers, M.A., Cuijpers, P.J.L.: Linearization of hybrid processes. Technical Report CS-Report 04-29, Eindhoven University of Technology, Department of Computer Science, The Netherlands (2004).Google Scholar
  21. 21.
    Schouten, R.: Simulation of hybrid processes. Master’s thesis, Eindhoven University of Technology (2005).Google Scholar
  22. 22.
    Rounds, W., Song, H., Compton, K.J.: Sphin: A model-checker for reconfigurable hybrid systems based on spin. Electronic Notes on Theoretical Computer Science 145 (2006) 167–183.CrossRefGoogle Scholar
  23. 23.
    van Putten, A.: Behavioural hybrid process calculus parser and translator to Modelica. Master’s thesis, University of Twente (2006).Google Scholar
  24. 24.
    Wijs, A.J., Fokkink, W.J.: From χt to μcrl: Combining performance and functional analysis. In Press, I.C.S., ed.: The 10th Conference on Engineering of Complex Computer Systems, Shanghai, China (2005).Google Scholar
  25. 25.
    PAFESD Web site: Process algebras for electronic system designs

Copyright information

© Springer Science+Business Media, LLC 2008

Authors and Affiliations

  • Ka Lok Man
    • 1
  • Michel P. Schellekens
    • 1
  1. 1.Centre for Efficiency-Oriented Languages (CEOL), Department of Computer ScienceUniversity College Cork (UCC)CorkIreland

Personalised recommendations