Panellist position statement: some industrial experience with program verification

2005 ◽  
Vol 363 (1835) ◽  
pp. 2393-2394
Author(s):  
Roderick Chapman
Keyword(s):  
Software Engineering ◽  
Formal Methods ◽  
Programming Language ◽  
Program Verification ◽  
Position Statement ◽  
Software Systems ◽  
Engineering Company ◽  
Verification Tools ◽  
High Integrity ◽  
Verification Techniques

As the only obvious ‘industrial’ member of the panel, I would like to introduce myself and the work I am involved with. Praxis is a practising software engineering company that is well known for applying so-called ‘Formal Methods’ in the development of high-integrity software system. We are also responsible for the Spark programming language and verification tools ( John Barnes with Praxis High Integrity Systems 2003 ). Spark remains one of the very few technologies to offer a sound verification system for an industrially usable imperative programming language. Despite the popular belief that ‘no one does formal methods’, we (and our customers) regularly employ strong verification techniques on industrial-scale software systems. I would like to address three main points:

Validation and Verification of Software Systems Using Virtual Reality and Coloured Petri Nets

2007 ◽  
pp. 28-54
Author(s):  
Hyggo Almeida ◽  
Leandro Silva ◽  
Glauber Ferreira ◽  
Emerson Loureiro ◽  
Angelo Perkusich
Keyword(s):  
Virtual Reality ◽  
Embedded System ◽  
Petri Nets ◽  
Formal Methods ◽  
Software Tool ◽  
Software Systems ◽  
Coloured Petri Nets ◽  
Validation And Verification ◽  
Verification Techniques

Validation and verification techniques have been identified as suitable mechanisms to determine if the software meets the needs of the user and to verify if the software works correctly. However, the existing verification techniques do not support friendly visualization. Also, validation techniques with friendly visualization mechanisms do not allow the verification of the system’s correctness. In this chapter, we present a method for the validation and verification of software systems through the integration of formal methods and virtual reality. Furthermore, a software tool associated with such a method is also described along with an embedded system case study.

Validation and Verification of Software Systems Using Virtual Reality and Coloured Petri Nets

2009 ◽  
pp. 3361-3380
Author(s):  
Hyggo Oliveira de Almeida ◽  
Leandro Silva ◽  
Glauber Ferreira ◽  
Emerson Loureiro ◽  
Angelo Perkusich
Keyword(s):  
Virtual Reality ◽  
Embedded System ◽  
Petri Nets ◽  
Formal Methods ◽  
Software Tool ◽  
Software Systems ◽  
Coloured Petri Nets ◽  
Validation And Verification ◽  
Verification Techniques

Validation and verification techniques have been identified as suitable mechanisms to determine if the software meets the needs of the user and to verify if the software works correctly. However, the existing verification techniques do not support friendly visualization. Also, validation techniques with friendly visualization mechanisms do not allow the verification of the system’s correctness. In this chapter, we present a method for the validation and verification of software systems through the integration of formal methods and virtual reality. Furthermore, a software tool associated with such a method is also described along with an embedded system case study.

scholarly journals Software engineering and formal methods: SEFM 2019 special section

2021 ◽  
Vol 20 (2) ◽  
pp. 291-292
Author(s):  
Peter Csaba Ölveczky ◽  
Gwen Salaün
Keyword(s):  
Software Engineering ◽  
Formal Methods ◽  
Special Section

scholarly journals Software engineering and formal methods

2008 ◽  
Vol 51 (9) ◽  
pp. 54-59 ◽  
Author(s):  
Mike Hinchey ◽  
Michael Jackson ◽  
Patrick Cousot ◽  
Byron Cook ◽  
Jonathan P. Bowen ◽  
...  
Keyword(s):  
Software Engineering ◽  
Formal Methods
Sign in / Sign up

Export Citation Format

Share Document