Abstract
Simulink is widely accepted in industry for model-based designs. Verification of Simulink diagrams against contracts or implementations has attracted the attention of many researchers. We present a compositional assume-guarantee reasoning framework to provide a purely relational mathematical semantics for discrete-time Simulink diagrams, and then to verify the diagrams against the contracts in the same semantics in UTP. We define semantics for individual blocks and composition operators, and develop a set of calculation laws (based on the equational theory) to facilitate automated proof. An industrial safety-critical model is verified using our approach. Furthermore, all these definitions, laws, and verification of the case study are mechanised in Isabelle/UTP, an implementation of UTP in Isabelle/HOL.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Isabelle/UTP: https://www.cs.york.ac.uk/circus/isabelle-utp/.
- 3.
However, because the order of input or output ports matter, we define inouts as a sequence of inputs or outputs. By this way, the order information has kept in our translation.
- 4.
Sequential composition of blocks is the same as sequence of designs, and therefore has been defined in the theory of designs.
- 5.
Honeywell: https://www.honeywell.com/.
- 6.
D-RisQ: http://www.drisq.com/.
References
Add2: Jaguar Reduces Development Costs with MathWorks—Rapid Prototyping and Code Generation Tools. http://www.add2.co.uk/wp-content/uploads/add2JaguarUSERStory.pdf
Amalio, N., Cavalcanti, A., Miyazawa, A., Payne, R., Woodcock, J.: Foundations of the SysML for CPS modelling. Technical Report, INTO-CPS Deliverable, D2.2a (2016)
Arthan, R.D., Caseley, P., O’Halloran, C., Smith, A.: ClawZ: control laws in Z. In: Proceedings of 3rd IEEE International Conference on Formal Engineering Methods, ICFEM 2000, York, England, UK, 4–7 Sept 2000, pp. 169–176. IEEE Computer Society (2000). https://doi.org/10.1109/ICFEM.2000.873817
Bauer, S.S., David, A., Hennicker, R., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Moving from Specifications to Contracts in Component-Based Design. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering—Proceedings of 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 24 Mar–1 Apr 2012. Lecture Notes in Computer Science, vol. 7212, pp. 43–58. Springer (2012). https://doi.org/10.1007/978-3-642-28872-2_3
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)
Bhatt, D., Chattopadhyay, A., Li, W., Oglesby, D., Owre, S., Shankar, N.: Contract-based verification of complex time-dependent behaviors in avionic systems. In: Rayadurgam, S., Tkachuk, O. (eds.) Proceedings of 8th International Symposium on NASA Formal Methods, NFM 2016, Minneapolis, MN, USA, 7–9 June 2016. Lecture Notes in Computer Science, vol. 9690, pp. 34–40. Springer (2016). https://doi.org/10.1007/978-3-319-40648-0_3
Boström, P.: Contract-based verification of simulink models. In: Qin, S., Qiu, Z. (eds.) Proceedings of 13th International Conference on Formal Engineering Methods and Software Engineering , ICFEM 2011, Durham, UK, 26–28 Oct 2011. Lecture Notes in Computer Science, vol. 6991, pp. 291–306. Springer (2011). https://doi.org/10.1007/978-3-642-24559-6_21.
Boström, P., Wiik, J.: Contract-based verification of discrete-time multi-rate Simulink models. Softw. Syst. Model. 15(4), 1141–1161 (2016). https://doi.org/10.1007/s10270-015-0477-x
Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating discrete-time simulink to lustre. In: Alur, R., Lee, I. (eds.) Proceedings of Third International Conference on Embedded Software, EMSOFT 2003, Philadelphia, PA, USA, 13–15 Oct 2003. Lecture Notes in Computer Science, vol. 2855, pp. 84–99. Springer (2003). https://doi.org/10.1007/978-3-540-45212-6_7
Cavalcanti, A., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via circus
Cavalcanti, A., Clayton, P., O’Halloran, C.: Control law diagrams in circus. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) Proceedings of FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, 18–22 July 2005. Lecture Notes in Computer Science, vol. 3582, pp. 253–268. Springer (2005). https://doi.org/10.1007/11526841_18
Cavalcanti, A., Mota, A., Woodcock, J.: Simulink timed models for program verification. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods—Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. Lecture Notes in Computer Science, vol. 8051, pp. 82–99. Springer (2013). https://doi.org/10.1007/978-3-642-39698-4_6
Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) First Pernambuco Summer School on Software Engineering, Refinement Techniques in Software Engineering, PSSE 2004, Recife, Brazil, 23 Nov–5 Dec 2004, Revised Lectures. Lecture Notes in Computer Science, vol. 3167, pp. 220–268. Springer (2004). https://doi.org/10.1007/11889229_6
Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bosnacki, D., Wijs, A. (eds.) Proceedings of 23rd International Symposium on Model checking software, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, 7–8 Apr 2016. Lecture Notes in Computer Science, vol. 9641, pp. 38–56. Springer (2016). https://doi.org/10.1007/978-3-319-32582-8_3
Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. In preparation for Theoretical Computer Science (2017). arXiv:1712.10233
Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) 5th International Symposium on Unifying Theories of Programming, UTP 2014, Singapore, 13 May 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol. 8963, pp. 21–41. Springer (2014). https://doi.org/10.1007/978-3-319-14806-9_2
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: In: Proceedings of FDR3—A Modern Refinement Checker for CSP. Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 8413, pp. 187–201 (2014)
Hoare, C., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall (1998)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Hoare, C.A.R., Roscoe, A.W.: Programs as Executable Predicates. In: Proceedings of FGCS, pp. 220–228 (1984)
Jones, C.B.: Wanted: a compositional approach to concurrency, pp. 5–15. Springer, New York, NY (2003). https://doi.org/10.1007/978-0-387-21798-7_1.
Jones, R.B.: ClawZ—The Semantics of Simulink Diagrams. Lemma 1 Ltd. (2003)
Lee, E.A., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75, 1235–1245 (1987)
Li, W., Gérard, L., Shankar, N.: Design and verification of multi-rate distributed systems. In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 20–29. IEEE (2015)
Marian, N., Ma, Y.: Translation of Simulink Models to Component-based Software Models, pp. 274–280. Forlag uden navn (2007)
MathWorks: Simulink. https://www.mathworks.com/products/simulink.html
Meyer, B.: Applying “Design by Contract”. IEEE Comput. 25(10), 40–51 (1992). https://doi.org/10.1109/2.161279
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283. Springer (2002). https://doi.org/10.1007/3-540-45949-9
Object Management Group: OMG Systems Modeling Language (OMG SysML\(^{\rm TM}\)). Technical Report. Version 1.4 (2015). http://www.omg.org/spec/SysML/1.4/
OpenModelica. https://openmodelica.org/
Oppenheim, A.V., Willsky, A.S., Nawab, S.H.: Signals and Systems, 2nd edn. Prentice-Hall Inc, Upper Saddle River, NJ, USA (1996)
Preoteasa, V., Dragomir, I., Tripakis, S.: The refinement calculus of reactive systems. CoRR (2017). arXiv:1710.03979
Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. CoRR (2014). arXiv:1406.6035
ProofPower. http://www.lemma-one.com/ProofPower/index/index.html
Roy, P., Shankar, N.: SimCheck: a contract type system for Simulink. Innov. Syst. Softw. Eng. 7(2), 73 (2011). https://doi.org/10.1007/s11334-011-0145-4.
TeraSoft: The MathWorks in the Automotive Industry. http://www.terasoft.com.tw/product/doc/auto.pdf
Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(4), 14 (2011)
Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time simulink to lustre. ACM Trans. Embed. Comput. Syst. 4(4), 779–818 (2005). https://doi.org/10.1145/1113830.1113834
VeTSS: UK Research Institute in Verified Trustworthy Software Systems. https://vetss.org.uk/
Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) Integrated Formal Methods, pp. 40–66. Springer, Berlin Heidelberg, Berlin, Heidelberg (2004)
Zeyda, F., Ouy, J., Foster, S., Cavalcanti, A.: Formalising cosimulation models. In: Proceedings of Software Engineering and Formal Methods (2018). https://doi.org/10.1007/978-3-319-74781-1_31.
Acknowledgements
This project is funded by the National Cyber Security Centre (NCSC) through UK Research Institute in Verified Trustworthy Software Systems (VeTSS) [39]. The second author is partially supported by EPSRC grant CyPhyAssure, EP/S001190/1. We thank Honeywell and D-RisQ for sharing of the industrial case study.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Ye, K., Foster, S., Woodcock, J. (2020). Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP. In: Adamatzky, A., Kendon, V. (eds) From Astrophysics to Unconventional Computation. Emergence, Complexity and Computation, vol 35. Springer, Cham. https://doi.org/10.1007/978-3-030-15792-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-15792-0_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-15791-3
Online ISBN: 978-3-030-15792-0
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)