Abstract
Previously we proposed a strategy for translating control law diagrams into Circus. Combining elements from Z, CSP, and a refinement calculus, Circus captures functional and dynamic aspects of a diagram, and allows us to formally verify implementations. The main contributions of this paper are first to discuss a generalisation of the existing translation strategy, motivated by its mechanisation and application to sizable examples. Secondly, we present a tool, the Circus Producer, which automates the translation, and describe how its architecture facilitates subsequent development of further verification tools.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Adams, M., Clayton, P.: ClawZ: Cost-Effective Formal Verification of Control Systems. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 465–479. Springer, Heidelberg (2005)
Arthan, R., Caseley, P., O’Halloran, C., Smith, A.: ClawZ: Control laws in Z. In: 3rd International Conference on Formal Engineering Methods, September 2000, pp. 169–176. IEEE Computer Society Digital Library (2000)
Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for Translating Simulink Models into Input Language of a Model Checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006)
Capsi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating Discrete-Time Simulink to Lustre. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 84–99. Springer, Heidelberg (2003)
Cavalcanti, A.: Stateflow Diagrams in Circus. In: SBMF 2008, pp. 1–16 (2008)
Cavalcanti, A., Clayton, P., O’Halloran, C.: Control Law Diagrams in Circus. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253–268. Springer, Heidelberg (2005)
Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2–3), 146–181 (2003)
Chen, C., Dong, J.S.: Applying Timed Interval Calculus to Simulink Diagrams. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 74–93. Springer, Heidelberg (2006)
Freitas, L., Woodcock, J., Cavalcanti, A.: An Architecture for Circus Tools. In: SBMF 2007: Brazilian Symposium on Formal Methods (August 2007)
Krogh, B.: Approximating Hybrid System Dynamics for Analysis and Control. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, p. 2. Springer, Heidelberg (1999)
Krogh, B.: Recent Developments in Modeling and Analysis of Hybrid Dynamic Systems. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, p. 106. Springer, Heidelberg (1999)
Malik, P., Utting, M.: CZT: A Framework for Z Tools. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 65–84. Springer, Heidelberg (2005)
Miller, T., Freitas, L., Malik, P., Utting, M.: CZT Support for Z Extensions. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 227–245. Springer, Heidelberg (2005)
Oliveira, M., Cavalcanti, A., Woodcock, J.: Refining Industrial Scale Systems in Circus. In: Communicating Process Architectures. Concurrent Systems Engineering Series, vol. 62, pp. 281–309. IOS Press, Amsterdam (2004)
Oliveira, M., Cavalcanti, A., Woodcock, J.: Formal Development of Industrial-Scale Systems in Circus. Innovations in Systems and Software Engineering 1(2), 125–146 (2005)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects of Computing, Online First (2007)
Parr, T.: StringTemplate Engine, http://www.stringtemplate.org
Ranville, S., Black, P.E.: Automated Testing Requirements — Automotive Perspective. In: The Second International Workshop on Automated Program Analysis, Testing and Verification (May 2001)
The MathWorks, Inc. Simulink ® (1994–2008)
Woodcock, J., Cavalcanti, A.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zeyda, F., Cavalcanti, A. (2009). Mechanised Translation of Control Law Diagrams into Circus . In: Leuschel, M., Wehrheim, H. (eds) Integrated Formal Methods. IFM 2009. Lecture Notes in Computer Science, vol 5423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00255-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-00255-7_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00254-0
Online ISBN: 978-3-642-00255-7
eBook Packages: Computer ScienceComputer Science (R0)