Advertisement

Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

  • Kangfeng Ye
  • Simon Foster
  • Jim WoodcockEmail author
Chapter
Part of the Emergence, Complexity and Computation book series (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.

Notes

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.

References

  1. 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. 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. 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. 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. 5.
    Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)MathSciNetCrossRefGoogle Scholar
  6. 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. 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. 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-xCrossRefzbMATHGoogle Scholar
  9. 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. 10.
    Cavalcanti, A., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via circusGoogle Scholar
  11. 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. 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. 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. 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. 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. 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. 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. 18.
    Hoare, C., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall (1998)Google Scholar
  19. 19.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)Google Scholar
  20. 20.
    Hoare, C.A.R., Roscoe, A.W.: Programs as Executable Predicates. In: Proceedings of FGCS, pp. 220–228 (1984)Google Scholar
  21. 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. 22.
    Jones, R.B.: ClawZ—The Semantics of Simulink Diagrams. Lemma 1 Ltd. (2003)Google Scholar
  23. 23.
    Lee, E.A., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75, 1235–1245 (1987)CrossRefGoogle Scholar
  24. 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. 25.
    Marian, N., Ma, Y.: Translation of Simulink Models to Component-based Software Models, pp. 274–280. Forlag uden navn (2007)Google Scholar
  26. 26.
  27. 27.
    Meyer, B.: Applying “Design by Contract”. IEEE Comput. 25(10), 40–51 (1992).  https://doi.org/10.1109/2.161279CrossRefGoogle Scholar
  28. 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. 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. 30.
  31. 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. 32.
    Preoteasa, V., Dragomir, I., Tripakis, S.: The refinement calculus of reactive systems. CoRR (2017). arXiv:1710.03979
  33. 33.
    Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. CoRR (2014). arXiv:1406.6035
  34. 34.
  35. 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.CrossRefGoogle Scholar
  36. 36.
    TeraSoft: The MathWorks in the Automotive Industry. http://www.terasoft.com.tw/product/doc/auto.pdf
  37. 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)CrossRefGoogle Scholar
  38. 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.1113834CrossRefGoogle Scholar
  39. 39.
    VeTSS: UK Research Institute in Verified Trustworthy Software Systems. https://vetss.org.uk/
  40. 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)CrossRefGoogle Scholar
  41. 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.

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.University of YorkYorkUnited Kingdom

Personalised recommendations