Abstract
The ClawZ toolset has been successful in verifying that Ada code is correctly generated from Simulink models in an industrial setting, using the Z notation. D-RisQ is now extending this technique to new domains of the C programming language, which requires changes to their highly complex proof technique. In this paper, we present initial results in the technology transfer of the graphical PSGraph language to support this extension, and show feasibility of PSGraph for industrial use with strong maintainability requirements.
This work has been supported by EPSRC grants EP/J001058, EP/K503915, EP/M018407 and EP/N014758. The second author is supported by a SICSA Industrial Fellowship.
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
Similar content being viewed by others
Notes
- 1.
See www.mathworks.com.
- 2.
See www.dspace.com.
- 3.
As far as we know, this is the largest proof tactic ever made in terms of code size.
- 4.
Recently, several typed tactic language, e.g. Mtac [9], have been developed. They will have comparable static properties to PSGraph, albeit they do not have the dynamic inspection features Tinker provides.
- 5.
A subset of C called C\(\flat \) is used. It has been designed with safety critical applications in mind. C\(\flat \)’s formalisation in ProofPower is based on work by Norrish for the HOL system [6]. The formalisation is comparable to Frama-C, however it has not been designed to act as a framework for other analysis tools.
References
Grov, G., Kissinger, A., Lin, Y.: A graphical language for proof strategies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 324–339. Springer, Heidelberg (2013)
Grov, G., Kissinger, A., Lin, Y.: Tinker, tailor, solver, proof. In: UITP 2014, vol. 167 of ENTCS, pp. 23–34. Open Publishing Association (2014)
Klein, G.: Proof engineering considered essential. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 16–21. Springer, Heidelberg (2014)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207–220. ACM (2009)
Lin, Y., Bras, P.L., Grov, G.: Developing & debugging proof strategies by tinkering. In: TACAS (2016). to appear
Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1999)
O’Halloran, C.: Automated verification of code automatically generated from Simulink. ASE 20(2), 237–264 (2013)
O’Halloran, C.: Nose-gear velocity-a challenge problem for software safety. In: Australian System Safety Conference (ASSC 2014), Held in Melbourne 28–30, May 2014 (2014)
Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. J. Funct. Program. 25, e12 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Lin, Y., Grov, G., O’Halloran, C., G., P. (2016). A Super Industrial Application of PSGraph. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-33600-8_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33599-5
Online ISBN: 978-3-319-33600-8
eBook Packages: Computer ScienceComputer Science (R0)