nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Initial Steps Towards Assessing the Usability of a Verification Tool

verfasst von : Mansur Khazeev, Victor Rivera, Manuel Mazzara, Leonard Johard

Erschienen in: Proceedings of 5th International Conference in Software Engineering for Defence Applications

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In this paper we report the experience of using AutoProof for static verification of a small object oriented program. We identify the problems that emerge by this activity and classify them according to their nature. In particular, we distinguish between tool-related and methodology-related issues, and propose necessary changes to simplify both the tool and the method.

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 Evolving In-service Support Models for Secure Weapon Systems

Nächstes Kapitel The Agile Coordination Processes

A cipher for an integrated set of tools checking correctness in a broad sense [1, 2].

EVE (Eiffel Verification Environment). EVE is a development environment integrating formal verification with the standard tools.

Denoting the current object in Eiffel.

http://www.adacore.com/sparkpro/tokeneer/download.

J. King, A program verifier. Ph.D. thesis, School of Computer Science, Carnegie Mellon University, 1969

J. Woodcock, E.G. Aydal, R. Chapman, The Tokeneer Experiments (2010), pp. 405–430

E.M. Clarke Jr., O. Grumberg, D.A. Peled, Model Checking (MIT Press, Cambridge, MA, USA, 1999)

M. Documentation, Code contracts, https://msdn.microsoft.com/en-us/library/dd264808, Accessed in May 2017

G.T. Leavens, Y. Cheon, Design by contract with jml, 2003

J. Tschannen, C.A. Furia, M. Nordio, N. Polikarpova, Autoproof: auto-active functional verification of object-oriented programs, in Proceedings of 21st International Conference, TACAS 2015 (London, UK, 11–18 April 2015), pp. 566–580

N. Polikarpova, J. Tschannen, C.A. Furia, B. Meyer, Flexible invariants through semantic collaboration. In: Proceedings of the 19th International Symposium on Formal Methods, FM 2014 (Springer International Publishing, Singapore, 12–16 May 2014), pp. 514–530

K.R.M. Leino, This is boogie 2, Technical Report (June 2008)

N. Polikarpova, J. Tschannen, C.A. Furia, A fully verified container library, in FM 2015: Formal Methods, Lecture Notes in Computer Science (Springer, 2015)

10.

E.Z. Chair of Software Engineering. Autoproof tutorial

11.

A. Kogtenkov, Void safety. Ph.D. thesis, ETH Zurich, 2017

12.

B. Meyer, Touch of Class: Learning to Program Well with Objects and Contracts, 1st edn. (Springer Publishing Company, 2009)

13.

D. de Carvalho, Modularly reasoning in object-oriented programming using export status (unpublished, 2017)

14.

Z. Yan, M. Mazzara, E. Cimpian, A. Urbanec, Business process modeling: classifications and perspectives, in Business Process and Services Computing: 1st International Working Conference on Business Process and Services Computing, BPSC 2007 (Leipzig, Germany, 25–26 September 2007), p. 222

15.

M. Mazzara, A. Bhattacharyya, On modelling and analysis of dynamic reconfiguration of dependable real-time systems, in 2010 Third International Conference on Dependability (July 2010), pp. 173–181

16.

M. Mazzara, Deriving specifications of dependable systems: toward a method, in Proceedings of the 12th European Workshop on Dependable Computing, EWDC (2009)

17.

V. Rivera, N. Cataño, Translating Event-B to JML-Specified Java programs, in 29th ACM SAC, (Gyeongju, South Korea, 24–28 March 2014)

18.

V. Rivera, N. Cataño, T. Wahls, C. Rueda, Code generation for event-b. Int. J. Softw. Tools Technol. Transf. 19, 31–52 (2017)

19.

V. D’Silva, D. Kroening, G. Weissenbacher, A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circ. Syst. 27(7), 1165–1178 (2008)

20.

R. Razali, P. Garratt, Usability requirements of formal verification tools: a survey, J. Comput. Sci. 10(6), 1189–1198 (2010)

21.

C.A. Furia, C.M. Poskitt, J. Tschannen, The AutoProof verifier: usability by non-experts and on standard code, in Proceedings of the 2nd Workshop on Formal Integrated Development Environment (F-IDE), ed. by C. Dubois, P. Masci, D. Mery, vol. 187 (EPTCS, June 2015), pp. 42–55

Titel: Initial Steps Towards Assessing the Usability of a Verification Tool
verfasst von: Mansur Khazeev
Victor Rivera
Manuel Mazzara
Leonard Johard
Verlag: Springer International Publishing
Buch: Proceedings of 5th International Conference in Software Engineering for Defence Applications
Print ISBN: 978-3-319-70577-4

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

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-70578-1_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner