scholarly journals Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM

2021 ◽  
Author(s):  
Simon Foster ◽  
Yakoub Nemouchi ◽  
Mario Gleirscher ◽  
Ran Wei ◽  
Tim Kelly
Keyword(s):  
Formal Methods ◽  
Formal Proof ◽  
Security Requirements ◽  
Computer Assisted ◽  
Critical Systems ◽  
Diverse Range ◽  
Functional Specification ◽  
Assurance Cases ◽  
Verification Techniques

AbstractAssurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as the use of formal methods is contingent on models that are validated by informal processes. Consequently, assurance techniques should support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language, called Isabelle/SACM, supporting the computer-assisted construction of assurance cases compliant with the OMG Structured Assurance Case Meta-Model. The use of Isabelle/SACM guarantees well-formedness, consistency, and traceability of assurance cases, and allows a tight integration of formal and informal evidence of various provenance. In particular, Isabelle brings a diverse range of automated verification techniques that can provide evidence. To validate our approach, we present a substantial case study based on the Tokeneer secure entry system benchmark. We embed its functional specification into Isabelle, verify its security requirements, and form a modular security case in Isabelle/SACM that combines the heterogeneous artifacts. We thus show that Isabelle is a suitable platform for critical systems assurance.

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.

A REVIEW APPROACH TO DETECTING VIOLATIONS OF CONSISTENCY BETWEEN SPECIFICATION AND PROGRAM STRUCTURES

2008 ◽  
Vol 18 (08) ◽  
pp. 1013-1042
Author(s):  
YUTING CHEN ◽  
SHAOYING LIU ◽  
W. ERIC WONG
Keyword(s):  
Program Verification ◽  
Formal Proof ◽  
Black Box ◽  
Program Review ◽  
Prototype Tool ◽  
Essential Idea ◽  
Black Box Testing ◽  
Structural Consistency ◽  
Verification Techniques

The application of specification-based program verification techniques (e.g., black-box testing, formal proof) faces strong challenges in practice when the gap between the structure of a specification and that of its program is large. This paper describes a view-based program review approach to addressing these challenges. The essential idea of the approach is first to derive comparable views from the specification and program, and then detect and eliminate the violations of structural consistency in the program views on the basis of a set of criteria. We also developed a prototype tool to support the review approach, and conducted a case study to assess the effectiveness of the approach.

scholarly journals Integration of Formal Proof into Unified Assurance Cases - With Isabelle/SACM

ITNOW ◽  
2021 ◽  
Vol 63 (3) ◽  
pp. 66-66
Author(s):  
Simon Foster ◽  
Yakoub Nemouchi ◽  
Mario Gleirscher ◽  
Ran Wei ◽  
Tim Kelly
Keyword(s):  
Formal Methods ◽  
Formal Proof ◽  
Assurance Cases

Abstract The paper, by Simon Foster, Yakoub Nemouchi, Mario Gleirscher, Ran Wei and Tim Kelly, published in The Formal Aspects of Computing—Applicable Formal Methods (June 2021), explores the introduction of Isabelle/SACM into formal methods of assurance.

scholarly journals Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root

2019 ◽  
Vol 26 (4) ◽  
pp. 520-533
Author(s):  
Vassil Todorov ◽  
Safouan Taha ◽  
Frederic Boulanger ◽  
Armando Hernandez
Keyword(s):  
Linear Interpolation ◽  
Formal Proof ◽  
Unit Testing ◽  
Square Root ◽  
Critical Systems ◽  
Safety Properties ◽  
Driver Assistance Systems ◽  
Deductive Proof ◽  
Automotive Embedded Software ◽  
Verification Techniques

For many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is deductive proof. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing.In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in the automotive embedded software.

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.

Teaching Computer Based Historical Data Analysis

1994 ◽  
Vol 6 (1) ◽  
pp. 52-58 ◽  
Author(s):  
Charles Anderson ◽  
Robert J. Morris
Keyword(s):  
Data Analysis ◽  
Social History ◽  
Historical Data ◽  
Good Practice ◽  
Computer Assisted ◽  
Historical Data Analysis ◽  
University Of Edinburgh ◽  
Computer Based ◽  
The University

A case study ofa third year course in the Department of Economic and Social History in the University of Edinburgh isusedto considerandhighlightaspects of good practice in the teaching of computer-assisted historical data analysis.

Formal Verification of Control System Software

2019 ◽  
Author(s):  
Pierre-Loïc Garoche
Keyword(s):  
Control System ◽  
Formal Verification ◽  
Formal Analysis ◽  
Critical Systems ◽  
System Software ◽  
Unified Approach ◽  
Verification Methods ◽  
Autonomous Cars ◽  
Computer Scientists ◽  
Verification Techniques

The verification of control system software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive. The failure of controller software can cost people their lives. This book provides control engineers and computer scientists with an introduction to the formal techniques for analyzing and verifying this important class of software. Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. The book provides a unified approach that is geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. It presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software. As the autonomy of critical systems continues to increase—as evidenced by autonomous cars, drones, and satellites and landers—the numerical functions in these systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.

scholarly journals Better state pictures facilitating state machine characteristic conjecture

2021 ◽  
Author(s):  
Dang Duy Bui ◽  
Kazuhiro Ogata
Keyword(s):  
Virtual Machines ◽  
Mutual Exclusion ◽  
State Machine ◽  
Formal Proof ◽  
The State ◽  
Lessons Learned ◽  
Java Virtual Machines ◽  
Core Part ◽  
Proximity Principle

AbstractThe mutual exclusion protocol invented by Mellor-Crummey and Scott (called MCS protocol) is used to exemplify that state picture designs based on which the state machine graphical animation (SMGA) tool produces graphical animations should be better visualized. Variants of MCS protocol have been used in Java virtual machines and therefore the 2006 Edsger W. Dijkstra Prize in Distributed Computing went to their paper on MCS protocol. The new state picture design of a state machine formalizing MCS protocol is assessed based on Gestalt principles, more specifically proximity principle and similarity principle. We report on a core part of a formal verification case study in which the new state picture design and the SMGA tool largely contributed to the successful completion of the formal proof that MCS protocol enjoys the mutual exclusion property. The lessons learned acquired through our experiments are summarized as two groups of tips. The first group is some new tips on how to make state picture designs. The second one is some tips on how to conjecture state machine characteristics by using the SMGA tool. We also report on one more case study in which the state picture design has been made for the mutual exclusion protocol invented by Anderson (called Anderson protocol) and some characteristics of the protocol have been discovered based on the tips.

Sign in / Sign up

Export Citation Format

Share Document