Abstract
Control diagrams are routinely used by engineers in the design of control systems. Yet, currently the formal verification of programs that implement the diagrams is a challenge. We present a strategy to translate block diagrams to Circus, a notation that combines Z, CSP, and a refinement calculus. This work is based on existing tools that produce Z and CSP specifications from discrete-time block diagrams. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of these diagrams, and can cover a wider range of blocks. Moreover, the Circus refinement calculus can be used to verify implementations, and reason about the block diagrams.
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
The MathWorks. Simulink, http://www.mathworks.com/products/simulink
Arthan, R., Caseley, P., O’Halloran, C., Smith, A.: ClawZ: Control laws in Z. In: ICFEM 2000, pp. 169–176. IEEE Press, Los Alamitos (2000)
Blow, J., Galloway, A.: Generalised Substitution Language and Differentials. In: Bert, D., et al. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 396–415. Springer, Heidelberg (2002)
Boulton, R.J., Hardy, R., Martin, U.: A Hoare-Logic for Single-Input Single-Output Continuous-Time Control Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 113–125. Springer, Heidelberg (2003)
Caspi, 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.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2 - 3), 146–181 (2003)
Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC—A Refinement Calculus for Z. Formal Aspects of Computing 10(3), 267–289 (1999)
Fischer, C.: How to Combine Z with a Process Algebra. In: P. Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 5–25. Springer, Heidelberg (1998)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Jersak, M., Ziegenbein, D., Wolf, F., Richter, K., Ernst, R.: Embedded System Design using the SPI Workbench. In: 3rd International Forum on Design Languages (2000)
King, D.J., Arthan, R.D., Winnersh, I.C.L.: Development of Practical Verification Tools. ICL Systems Journal 11(1) (1996)
Mahony, B.: Workshop on Formalising Continuous Mathematics. The DOVE Approach to the Design of Complex Dynamic Processes, 167–187 (2002)
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)
O’Halloran, C., Smith, A.: Verification of Picture Generated Code. In: ASE 1999, pp. 127–136. IEEE Press, Los Alamitos (1999)
Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Refining Industrial Scale Systems in Circus. In: CPA 2004, September 2004, pp. 281–309. IOS Press, Amsterdam (2004)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)
Spencer, C.: Model Checking for Stateflow Diagram with Floating Point Variables and Complex Expressions. Master’s thesis, Carnegie Mellon University (2002)
Tiwari, A.: Formal Semantics and Analysis Methods for Simulink Stateflow Models. Technical report, SRI International (2002), http://www.csl.sri.com/~tiwari/stateflow.html
Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of Circus. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Woodcock, J.C.P., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cavalcanti, A., Clayton, P., O’Halloran, C. (2005). Control Law Diagrams in Circus . In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_18
Download citation
DOI: https://doi.org/10.1007/11526841_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)