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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK (1990).
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. EACTS Monographs in Theoretical Computer Science. Springer-Verlag, New York (2002).
Man, K.L., Schiffelers, R.R.H.: Formal specification and analysis of hybrid systems. PhD thesis, Eindhoven University of Technology (2006).
Cuijpers, P.J.L.: Hybrid process algebra. PhD thesis, Eindhoven University of Technology (2004).
Bergstra, J.A., Middelburg, C.A.: Process algebra for hybrid systems. Theoretical Computer Science 335(2/3) (2005) 215–280.
Krilavičius, T.: Hybrid techniques for hybrid systems. PhD thesis, University of Twente (2006).
Plotkin, G.D.: A structural approach to operational semantics. Technical Report DIAMI FN-19, Computer Science Department, Aarhus University (1981).
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.
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).
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.
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).
Krilavi\breve{\text{c}}ius, T.: Study of tools interoperability. Technical Report TR-CTIT-07-01, University of Twente, The Netherlands (2007).
OpenModelica System Web site: Openmodelica system http://www.ida.liu.se/~pelab/modelica/.
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.
Modelica Association: Modelica — A unified object-oriented language for physical systems modeling, http://www.modelica.org. (2002).
Lynch, N., Segala, R., Vaandrager, F.: Hybrid I/O automata. Information and Computation 185 (1) (2003) 105–157.
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.
Frehse, G.: Language overview v.0.2.2.1 for PHAVer v.0.2.2, www.cs.ru.nl/~goranf. (2004).
Khadim, U.: A comparative study of process algebras for hybrid systems. Technical Report CS-Report 06-23, Eindhoven University of Technology, The Netherlands (2006).
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).
Schouten, R.: Simulation of hybrid processes. Master’s thesis, Eindhoven University of Technology (2005).
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.
van Putten, A.: Behavioural hybrid process calculus parser and translator to Modelica. Master’s thesis, University of Twente (2006).
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).
PAFESD Web site: Process algebras for electronic system designs http://digilander.libero.it/systemcfl/pafesd/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Man, K.L., Schellekens, M.P. (2008). Interoperability of Performance and Functional Analysis for Electronic System Designs in Behavioural Hybrid Process Calculus (BHPC). In: Castillo, O., Xu, L., Ao, SI. (eds) Trends in Intelligent Systems and Computer Engineering. Lecture Notes in Electrical Engineering, vol 6. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-74935-8_27
Download citation
DOI: https://doi.org/10.1007/978-0-387-74935-8_27
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-74934-1
Online ISBN: 978-0-387-74935-8
eBook Packages: EngineeringEngineering (R0)