Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Introduction to the First Issue of FoMaC Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Verified Change

verfasst von : Klaus Havelund, Rahul Kumar

Erschienen in: Transactions on Foundations for Mastering Change I

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We present the textual wide-spectrum modeling and programing language K, which has been designed for representing graphical SysML models, in order to provide semantics to SysML, and pave the way for analysis of SysML models. The current version is supported by the Z3 SMT theorem prover, which allows to prove consistency of constraints. The language is intended to be used by engineers for designing space missions, and in particular NASA’s proposed mission to Jupiter’s moon Europa. One of the challenges facing software development teams is the notion of change: the fact that code changes over time, and the subsequent problem of demonstrating that no harm has been done due to a change. K is in this paper being applied to demonstrate how change can be perceived as a software verification problem, and hence verified using more traditional software verification techniques.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Model Patterns
Nächstes Kapitel Good Change and Bad Change: An Analysis Perspective on Software Evolution
Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
2.
Allen, J.F.: Towards a general theory of action and time. Artif. Intell. 23, 123–154 (1984)CrossRefMATH
3.
4.
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Texts in Computer Science. Springer, New York (1998)CrossRefMATH
5.
Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: static driver verification with under 4 % false alarms. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pp. 35–42. FMCAD Inc. (2010)
6.
7.
Bjørner, D., Jones, C.B.: Formal Specification and Software Development. Prentice Hall International, Englewood Cliffs (1982). ISBN: 0-13-880733-7MATH
8.
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53–64, Wrocław, Poland, August 2011
9.
Bubel, R., Hähnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 120–134. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-45231-8_​9
10.
11.
12.
13.
14.
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-Oriented Systems. Springer, London (2005)MATH
15.
16.
George, C., Haff, P., Havelund, K., Haxthausen, A., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Specification Language. The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead (1992)MATH
17.
George, C., Haxthausen, A.: The logic of the RAISE specification language. In: Bjørner, D., Henson, M. (eds.) Logics of Specification Languages. Monographs in Theoretical Computer Science, pp. 349–399. Springer, Heidelberg (2008)CrossRef
18.
Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Annual Design Automation Conference, pp. 466–471. ACM (2009)
19.
20.
Hähnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Giachino, E., Hähnle, R., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 1–37. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40615-7_​1 CrossRef
21.
22.
Havelund, K.: Closing the gap between specification, programming: VDM\(^{++}\) and Scala. In: Korovina, M., Voronkov, A. (eds.) HOWARD-60: Higher-Order Workshop on Automated Runtime Verification and Debugging, EasyChair Proceedings, Manchester, vol. 1, December 2011
23.
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. STTT 2(4), 366–381 (2000)CrossRefMATH
24.
Havelund, K., Visser, W.: Program model checking as a new trend. STTT 4(1), 8–20 (2002)CrossRef
25.
26.
Hentschel, M., Käsdorf, S., Hähnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55–70. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-10181-1_​4
27.
Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)
28.
29.
Jackson, D., Abstractions, S.: Logic, Language, and Analysis. The MIT Press, Cambridge (2012)
30.
31.
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall, Upper Saddle River (1990). ISBN: 0-13-880733-7MATH
32.
Jones, C.B., Shaw, R.C. (eds.): Case Studies in Systematic Software Development. Prentice Hall International, Upper Saddle River (1990). ISBN: 0-13-880733-7MATH
33.
34.
Kahrs, S., Sannella, D., Tarlecki, A.: The definition of Extended ML: a gentle introduction. Theor. Comput. Sci. 173, 445–484 (1997)MathSciNetCrossRefMATH
35.
Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31424-7_​54 CrossRef
36.
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-17511-4_​20 CrossRef
37.
Milner, R., Tofte, M., Harper, R. (eds.): The Definition of Standard ML. MIT Press, Cambridge (1997). ISBN: 0-262-63181-4
38.
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, New York (1994)MATH
39.
40.
Odersky, M.: Contracts for Scala. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 51–57. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-16612-9_​5 CrossRef
41.
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). doi:10.​1007/​3-540-55602-8_​217
42.
Person, S., Dwyer, M.B., Elbaum, S., Păsăreanu, C.S.: Differential symbolic execution. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 226–237. ACM (2008)
43.
44.
45.
46.
47.
Spivey, J.M.: Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, New York (1988)MATH
48.
Steffen, B.: LNCS transactions on foundations for mastering change: preliminary manifesto. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS. Theoretical Computer Science and General Issues, vol. 8803, pp. 514–517. Springer, Heidelberg (2014)
49.
50.
51.
Wirth, N.: Program development by stepwise refinement. Commun. ACM (CACM) 14, 221–227 (1971)CrossRefMATH
52.
Woodcock, J., Davies, J.: Using Z. Specification, Refinement, and Proof. Prentice-Hall, New York (1996)MATH
Metadaten
Titel
Verified Change
verfasst von
Klaus Havelund
Rahul Kumar
Copyright-Jahr
2016
Buch
Transactions on Foundations for Mastering Change I

Print ISBN: 978-3-319-46507-4

Electronic ISBN: 978-3-319-46508-1

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46508-1_5