Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

  • Chapter
  • First Online:
From Astrophysics to Unconventional Computation

Part of the book series: Emergence, Complexity and Computation ((ECC,volume 35))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    ClawZ: http://www.lemma-one.com/clawz_docs/.

  2. 2.

    Isabelle/UTP: https://www.cs.york.ac.uk/circus/isabelle-utp/.

  3. 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. 4.

    Sequential composition of blocks is the same as sequence of designs, and therefore has been defined in the theory of designs.

  5. 5.

    Honeywell: https://www.honeywell.com/.

  6. 6.

    D-RisQ: http://www.drisq.com/.

References

  1. Add2: Jaguar Reduces Development Costs with MathWorks—Rapid Prototyping and Code Generation Tools. http://www.add2.co.uk/wp-content/uploads/add2JaguarUSERStory.pdf

  2. 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)

    Google Scholar 

  3. 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

  4. 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

  5. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)

    Article  MathSciNet  Google Scholar 

  6. 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

  7. 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.

  8. 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

    Article  MATH  Google Scholar 

  9. 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

  10. Cavalcanti, A., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via circus

    Google Scholar 

  11. 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

  12. 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

  13. 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

  14. 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

  15. 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

  16. 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

  17. 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)

    Google Scholar 

  18. Hoare, C., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall (1998)

    Google Scholar 

  19. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)

    Google Scholar 

  20. Hoare, C.A.R., Roscoe, A.W.: Programs as Executable Predicates. In: Proceedings of FGCS, pp. 220–228 (1984)

    Google Scholar 

  21. 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.

  22. Jones, R.B.: ClawZ—The Semantics of Simulink Diagrams. Lemma 1 Ltd. (2003)

    Google Scholar 

  23. Lee, E.A., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75, 1235–1245 (1987)

    Article  Google Scholar 

  24. 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)

    Google Scholar 

  25. Marian, N., Ma, Y.: Translation of Simulink Models to Component-based Software Models, pp. 274–280. Forlag uden navn (2007)

    Google Scholar 

  26. MathWorks: Simulink. https://www.mathworks.com/products/simulink.html

  27. Meyer, B.: Applying “Design by Contract”. IEEE Comput. 25(10), 40–51 (1992). https://doi.org/10.1109/2.161279

    Article  Google Scholar 

  28. 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

  29. 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/

  30. OpenModelica. https://openmodelica.org/

  31. Oppenheim, A.V., Willsky, A.S., Nawab, S.H.: Signals and Systems, 2nd edn. Prentice-Hall Inc, Upper Saddle River, NJ, USA (1996)

    Google Scholar 

  32. Preoteasa, V., Dragomir, I., Tripakis, S.: The refinement calculus of reactive systems. CoRR (2017). arXiv:1710.03979

  33. Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. CoRR (2014). arXiv:1406.6035

  34. ProofPower. http://www.lemma-one.com/ProofPower/index/index.html

  35. 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.

    Article  Google Scholar 

  36. TeraSoft: The MathWorks in the Automotive Industry. http://www.terasoft.com.tw/product/doc/auto.pdf

  37. 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)

    Article  Google Scholar 

  38. 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

    Article  Google Scholar 

  39. VeTSS: UK Research Institute in Verified Trustworthy Software Systems. https://vetss.org.uk/

  40. 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)

    Chapter  Google Scholar 

  41. 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.

Download references

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

  1. University of York, York, United Kingdom

    Kangfeng Ye, Simon Foster & Jim Woodcock

Authors
  1. Kangfeng Ye
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Simon Foster
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jim Woodcock
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jim Woodcock .

Editor information

Editors and Affiliations

  1. Unconventional Computing Laboratory, University of the West of England, Bristol, UK

    Andrew Adamatzky

  2. Joint Quantum Centre, Durham University, Durham, UK

    Vivien Kendon

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

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

Publish with us

Policies and ethics

Search

Navigation