Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets Read chapter Read first chapter

2016 | OriginalPaper | Chapter

A Super Industrial Application of PSGraph

Authors : Yuhui Lin, Gudmund Grov, Colin O’Halloran, Priiya G.

Published in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Mechanized Refinement of Communication Models with TLA
next chapter The Hemodialysis Machine Case Study
Footnotes
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.
 
Literature
1.
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)CrossRef
2.
Grov, G., Kissinger, A., Lin, Y.: Tinker, tailor, solver, proof. In: UITP 2014, vol. 167 of ENTCS, pp. 23–34. Open Publishing Association (2014)
3.
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)CrossRef
4.
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)
5.
Lin, Y., Bras, P.L., Grov, G.: Developing & debugging proof strategies by tinkering. In: TACAS (2016). to appear
6.
Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1999)
7.
O’Halloran, C.: Automated verification of code automatically generated from Simulink. ASE 20(2), 237–264 (2013)
8.
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)
9.
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)MathSciNetCrossRefMATH
Metadata
Title
A Super Industrial Application of PSGraph
Authors
Yuhui Lin
Gudmund Grov
Colin O’Halloran
Priiya G.
Copyright Year
2016
Book
Abstract State Machines, Alloy, B, TLA, VDM, and Z

Print ISBN: 978-3-319-33599-5

Electronic ISBN: 978-3-319-33600-8

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-33600-8_28

Premium Partner

    Image Credits