Abstract
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools.
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
Notes
- 1.
Unified Modelling Language. http://www.uml.org/.
- 2.
Systems Modelling Language. http://www.omgsysml.org/.
- 3.
- 4.
The square brackets are not used in Isabelle; we add them for readability.
- 5.
References
Miyazawa, A., Ribieiro, P., Li, W., Cavalcanti, A., Timmis, J.: Automatic property checking of robotic applications. In: International Conference on Intelligent Robots and Systems (IROS), pp. 3869–3876. IEEE (2017)
Miyazawa, M., Cavalcanti, A., Ribeiro, P., Li, W., Woodcock, J., Timmis, J.: Robochart reference manual. Technical report, University of York (June 2018). https://cs.york.ac.uk/circus/RoboCalc/assets/robochart-reference.pdf
Hoare, T., He, J.: Unifying Theories of Programming. Prentice-Hall, London (1998)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Form. Asp. Comput. 21, 3–32 (2009)
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. Submitted to Theoretical Computer Science (Dec 2017). Preprint: arXiv:1712.10233
Foster, S., Ye, K., Cavalcanti, A., Woodcock, J.: Calculational verification of reactive programs with reactive relations and Kleene algebra. In: Desharnais, J. et al. (eds.) RAMiCS 2018. LNCS, vol. 11194, pp. 205–224. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02149-8_13
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)
Foster, S., Zeyda, F., Woodcock, J.: Unifying heterogeneous state-spaces with lenses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 295–314. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_17
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_2
Sherif, A., Cavalcanti, A., He, J., Sampaio, A.: A process algebraic framework for specification and validation of real-time systems. Form. Asp. Comput. 22(2), 153–191 (2010)
Bresciani, R., Butterfield, A.: A UTP semantics of pGCL as a homogeneous relation. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 191–205. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_14
Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J.: Towards a UTP semantics for modelica. In: Bowen, J.P., Zhu, H. (eds.) UTP 2016. LNCS, vol. 10134, pp. 44–64. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52228-9_3
Hilder, J., Owens, N., Neal, M., Hickey, P., Cairns, S., Kilgour, D., Timmis, J., Tyrrell, A.: Chemical detection using the receptor density algorithm. IEEE Trans. Syst. Man Cybern. 42(6), 1730–1741 (2012)
Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006). https://doi.org/10.1007/11889229_6
Santos, T., Cavalcanti, A., Sampaio, A.: Object-orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 18–37. Springer, Heidelberg (2006). https://doi.org/10.1007/11768173_2
Foster, S., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying theories of time with generalised reactive processes. Inf. Process. Lett. 135, 47–52 (2018)
Feliachi, A., Gaudel, M.-C., Wolff, B.: Unifying theories in Isabelle/HOL. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 188–206. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16690-7_9
Foster, S., et al.: Stateful-failure reactive designs in Isabelle/UTP. Technical report, University of York (2018). http://eprints.whiterose.ac.uk/129768/
Zhan, N., Kang, E.Y., Liu, Z.: Component publications and compositions. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 238–257. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14521-6_14
Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Berlin (1998)
Morgan, C., Vickers, T.: On the Refinement Calculus. Springer, Berlin (1992)
Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_9
McEwan, A.: Concurrent Program Development in Circus. Ph.D. thesis, Oxford University (2006)
Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. ENCTS 55(3), 357–369 (2001)
Miyazawa, A., Cavalcanti, A.: Refinement-oriented models of stateflow charts. Sci. Comput. Program. 77(10–11) (2012)
Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., Mallet, A.: Model checking real-time properties on the functional layer of autonomous robots. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 383–399. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_24
Acknowledgements
This work is funded by the EPSRC projects RoboCalc (RoboCalc Project: https://www.cs.york.ac.uk/circus/RoboCalc/) (Grant EP/M025756/1) and CyPhyAssure (CyPhyAssure Project: https://www.cs.york.ac.uk/circus/CyPhyAssure/) (Grant EP/S001190/1), and the Royal Academy of Engineering.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Foster, S., Baxter, J., Cavalcanti, A., Miyazawa, A., Woodcock, J. (2018). Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. In: Bae, K., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2018. Lecture Notes in Computer Science(), vol 11222. Springer, Cham. https://doi.org/10.1007/978-3-030-02146-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-02146-7_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02145-0
Online ISBN: 978-3-030-02146-7
eBook Packages: Computer ScienceComputer Science (R0)