See discussions, stats, and author profiles for this publication at: [Link]

net/publication/339399696

Existing Tools for Formal Verification and Formal Methods

Research · February 2020

CITATIONS READS
2 2,102

1 author:

Wambura Wasira
Lewis University
4 PUBLICATIONS 5 CITATIONS

SEE PROFILE

Some of the authors of this publication are also working on these related projects:

Research in Computer Science View project

Major Research Areas in Computer Science View project

All content following this page was uploaded by Wambura Wasira on 21 February 2020.

The user has requested enhancement of the downloaded file.

W. Wasira., MS Computer Science Student, Lewis University

Abstract— This paper is a summary of the themes conditions to confirm that it produces the output as it is
presented in two papers that report on the use of required to do so; adding that testing and simulation is
formal methods in the software development capable of sampling functional properties but limited in
industries. It will also present one industrial verifying safety and security properties of software.
application – Airbus A340 and A380 flight control
system that has incorporated formal methods in its The paper also introduces formal methods, categorizing
program development cycle. These papers also them in two separate categories: Model checkers that
describe how relevant these formal methods are in check the design with respect to the specified properties
conducting software verification and validation when and return results on whether the model satisfied the
incorporated in the development of software. The final specified properties; whether the model has not satisfied
section of this paper will present a summary of a the specified properties and if the properties were not
research conducted on formal method SCADE for satisfied, it produces a counter example that would satisfy
verifying Airbus’s A340 and A380 flight control the specification of the program. Model checkers also
systems. The paper “Survey of Existing Tools for produce indeterminate output in which the checker
Formal Verification” presents a report of a survey of displays areas of the state space where cannot compute
formal verification tools developed and adopted for results in a reasonable amount of time. The second
verification of software in the respective domains. The category outlined are Theorem provers, more powerful
Formal Methods: Practice and Experience reports than model checkers, they combine automated techniques
findings of a survey of the adaptation of formal with manual proof to prove correctness of a program’s
verification methods in software development algorithm.
industries.
Like computer languages, formal methods are also
Index Terms— Formal Verification, Formal designed for use at different levels of abstractions. This
Methods, SCADE, Airbus knowledge has given rise to high-level formal tools that
are used to prove specification and low-level tools that are
I. INTRODUCTION used for reachability and program correctness. The report
classified available tools based on the tools’ capabilities
II. SURVEY OF EXISTING TOOLS FOR FORMAL and usage:
VERIFICATION
1) Tools for Verifying Correctness of a Model:
The paper titled Survey of Existing tools for Formal
Verification presents the findings of a survey conducted Tools used for verifying correctness of abstract models
in assessing the capabilities of commercial as well as open do not assist in the creation of a model, instead they can
source formal verification tools and the way in which they be used to test out ideas prior to implementation. The tools
can be useful in digital design workflow. The paper first that are used for verifying abstract models are often
presents an introduction of Formal methods and tools language specific, so models must be create using the
followed by a description of tools for checking abstraction specific language of these tools. These tools include Spin,
models, hardware description language, correctness of Uppaal, SMV, NuSMV, FDR, Alloy, and the Simulink
software as well as tools for creating provably correct Design Verifier.
software designs. The authors add, what systems require
are suitable automated mathematical approaches that are
Tools for verifying actual design description. These
able to exhaustively check the state space of the system
tools are further categorized as software verifiers which
without actually running the code or perform analytics of
are described as limited in their capabilities in that they
a program.
can only check simple properties. They include: Frama-
C, BLAST, Java Pathfinder, Spark ADA, and Malpas and
The first part of this paper briefly outlines the limitations Hardware Description Language (HDL) Verification
of Testing and Simulation explaining that testing and tools which were produced due to developers demand for
simulation alone provides a system with a variety of input
checking hardware designs; this in turn enabled the authors, formal methods in testing software, still requires
research into and production of these tools. They include further research. The paper does not describe how
SAT solvers, BDDs, ROBDDs and the SMT solvers. formal methods can be used in maintenance and
evolution of programs (Woodcock, Larsen, Bicarregui,
2) Tools for creating provably correct design: Fitzgerald, 2009). [1]

Based on set theory, these tools provide a formal One of the surveys conducted, by Austin and Parkin
framework and methodology for mathematically 1993, revealed that majority of the industry heads made
modeling and proving systems’ properties. They possess use of model-oriented formalism i.e. VDM and that they
the capabilities of tackling large problems as long as they focused more on specification rather than verification.
are configured to be adapted for the domain of the Furthermore, the surveys conducted by Bloomfield and
problem area. This can be achieved by narrowing the Craigen and his colleagues, focused on model-oriented
semantics to deal with a specific problem. They include approaches i.e. process calculus (CSP) and verification
VDM and Z, B, Event-B and Rodin. environments. The case studies are of small-scale
systems. One challenge presented with regard to the use
III. FORMAL METHODS: PRACTICE AND EXPERIENCE of formal verification tools is the that immaturity of
theories and tool bases resulted in case study subjects
This paper reports review of major publications of
requiring higher levels of effort to make use of these
surveys conducted to collect information of the use of
formal method tools and theories. The main reason
formal method in industrial software development
being, tools that are developed are not transferred across
projects. This report also includes issues surrounding
platforms or research groups and that they often do not
industrial use of formal methods, future industrial wise
advance methodologically or theoretically.
use of these methods as well as the description of the
development of a verified repository as part of the
A technical report produced by Rushby aimed to explain
worldwide Verified Software Initiative. Subjects
to NASA stakeholders the benefits or adopting formal
discussed in this paper include Software Program
methods in the development and certification of critical
Verification; Specification, Verification and Reasoning
systems in the aerospace domain, the report concluded
about Programs; Mathematical Logic as well as
that academicians saw formal methods as inevitable, but
Automatic Programming.
practitioners saw them as irrelevant. The report also
documents that the challenges that formal methods face
The authors define formal methods as mathematical
include weaknesses in notations, tools and education.
techniques, supported by tools to enable the
development of software and hardware systems. They
Section 3 of this paper presents a quantitative survey of
enable developers to analyze and verify models at any
industrial practice of formal methods from a number of
stage of the program development lifecycle including
industrial projects known to have employed formal
requirement engineering, specification, architecture,
techniques in software development tools and computing
design, implementation, testing, maintenance and
applications in transportation, finance, defense,
evolution of programs [1]
telecommunications, nuclear, healthcare, consumer
electronics, space, semantic web, resource planning,
In requirement engineering for example, formal methods
automated car parking, embedded software, engineering,
are described as useful in eliciting, articulating and
manufacturing as well as office and administration
representing requirements and that automated tools can
sectors.
help provide the support needed for checking
completeness traceability, verifiability and reusability of
Formal methods were shown to reduce the overall time
software and for supporting requirement evolution,
of developing the software and that the specification
diverse viewpoints and managing inconsistencies. In the
phase took the longest time to complete. More industries
specification stage, the methods help to develop precise
responded positively that formal methods improved
technical specifications of the purpose of the software. In
productivity and that once the code generation of the
architecture, formal methods help to develop software
tools had been bootstrapped, they helped to reduce the
architectural models. In software design, these methods
cost of the projects. Fewer industries reported increase in
support data refinement including state machine
the cost of production due to lack of precise complete
specification, abstraction functions and simulation
information about externally visible behavior of the
proofs. When the stage reaches implementation, formal
software product. However, once the code was
methods can be used to verify program source code to
implemented, the required behavior became clear. 92%
prove algorithm correctness theorem. According to the
of responses reported an increase in quality of their that the card was secure. Formal proofs were employed
products; 36% reported that formal methods improved to verify correspondence between the high-level abstract
detection of faults; 12% reported improvement in design, security policy model and the lower-level concrete
10% reported increased confidence in correctness; 10% architectural design. To ensure that the concrete design
reported improved understanding and 4% reported that obeyed the abstract security properties, the specification
they were able to identify faults and other issues early on and proofs were conducted using Z. The proofs revealed
in the development cycle. a small flaw in one of the minor protocols. During the
testing phase no errors were detected due to previous
Additionally, the authors report that 61% of respondents employment of formal verification methods.
agreed that the use of formal methods in their projects
was successful; 46% agreed that the techniques used Formal methods were deployed to specify and refine
were appropriate for the tasks required. In the survey AAMP Microprocessors. This project was not successful
report, 56% of respondents were satisfied with the tools due to complexity of the language and the only tools
employed in their projects and 75% of the respondents available were syntax and type checkers. In a subsequent
agreed they intend to make use of formal techniques. experiment on AAM5, a microprocessor with 500,000
transistors with performance between an Intel 386 and
Projects involved in this survey include: 486, PVS was used to formally prove correctness of its
microcode instructions. This experiment proved that it
The Transputer Project that involved the development of was it was technically possible to prove the correctness
microprocessor chips designed specifically for parallel of microcode. After that additional experiments were
processing with floating point units that are complex conducted on AAMP-FV using PVS and AAMP7 using
devices prone to device bugs; hence required months of ACL2 to prove whether that a line-by-line model of the
testing. Formal methods were used to verify correctness microcode adhered to a security policy when partitions
of the OCCAM programming language. Hoare logic a are allowed to communicate. This also yielded
formal method revealed errors in rounding of remainder encouraging results.
operations. This resulted in the development project
running three months faster than the alternative informal Airbus used SCADE tool which manages the evolution
development that ran concurrently. of a system model as requirements change. Benefits
reported included a significant decrease in coding errors
Railway Signaling and Train Control is a project for the Airbus A340 project including shorter
launched by MANTRA Transport and the Parisian requirement changes with improved traceability as well
Public Transporter Operator to computerize signaling as major improvement in productivity.
systems for controlling RER regional express network
commuter trains in Paris with the objective of increasing Another project involved in the survey include Maeslant
network traffic by 25% while preserving existing safety Kering Storm Surge Barrier, a movable barrier
levels. The software developed was known as SACEM protecting the port of Rotterdam from flooding during
consisting of 21,000 Modula-2 code. This code which adverse weather and sea conditions. The project
was regarded safety-critical was verified using a method employed formal modelling and verification in the
constructed in B language and the proofs were done analysis, design and realization phase of the system
interactively using automatically generated verification development cycle focusing on decision-making
conditions for the code. The formal techniques focused subsystem and its interfaces to the environment. Data
on ensuring safety of the overall system, these included and operations were modelled in Z and later embedded
online error detection, software validation and fault into a Promela model describing control. SPIN model
tolerance of the onboard-ground compound system. The checker was used in design validation, because of its
challenge in this project was the communication gap ease of use. Formal techniques employed did not detect
between verifiers and signaling engineers who were not many major defects in the system. 85% of the problems
familiar with the B-method. This was addressed by arose during development phase and 15% during the
providing the engineers with a French description reliability and acceptance test.
manual of the formal specification.
In the The Tokeneer Secure Entry System, Tokeneer ID
Mondex Smart Card an electronic cash system suitable Station (TIS) project was used to re-develop one
for low-value cash-like transactions developed by the component of the Tokeneer system. The SPARK tools
National Westminster Bank and Platform Seven. The written in Ada were used to generate verification
formal verification methods were employed to verify conditions for partial correctness and run-time errors.
 and program modules for software verification. Early
The \Mobile FeliCa" IC Chip Firmware was a project pilot projects in this challenge include Verified File
that used VDM++ and VDM. It is reported that from a Store, FreeRTOS a real-time performance mini-kernel,
quality perspective, more errors were found in the early Radio Spectrum Auctions, Cardiac Pacemaker and a
phases of the development than in other similar projects Hypervisor.
at FeliCa Networks. A total of 440 defects were detected
during the requirements and specification phases of the IV. AIRBUS ADAPTATION OF FORMAL VERIFICATION
project. Of the total errors, 278 were discovered with the TOOL SAFETY CRITICAL APPLICATION DEVELOPMENT
help of VDM++. 162 were discovered as a result of ENVIRONMENT (SCADE)
review of the model and out of these 116 were
discovered using VDMTools interpreter with test cases The following section presents the Airbus project that
against the executable VDM++ model. has been using formal verification tool SCADE. I chose
to present this project because Formal Methods:
The final part of this paper presents the authors Practice and Experience that presented the Airbus
observation of verification technology and formal project that was published in 2009, noted that Airbus,
methods, which include the lack of widespread adoption adopted formal methods ten years before this paper was
and use of these methods in the system development published. This means that, despite the claim that formal
practice with an exception on the development of safety- methods have not been widely adopted in systems
critical systems. The authors however do indicate that development industries, Airbus adopted these tools since
there has been gradual success in application of formal late 1990s. This to me suggests that if an industry such
methods to solve problems of industrial scale. They also as Airbus, that develops safety critical applications and
note that formal methods have potential in software provides services worldwide, has made formal methods
development in certain domains including code part and parcel of their development live cycles for 10
verification especially in traditional high-integrity years, then they must have realized the benefits of these
critical applications but need to be performed highly methods earlier than many other domains in other
technical specialists. industries.

Challenges include entry cost of formal methods. SCADE – Safety Critical Application Development
However, it is noted there could be decrease in cost with Environment is a formal method used by Airbus in a
repeated use. Emphasis for future use is on developing number of projects including the verification and
tools and tool chains as well as developing certification modelling the designs of the Airbus DO-178B Level A
for specialists’ practitioners and that automated formal controllers for their aircraft models A340 aircraft series
analysis is making it possible to have an impact on large- as well as A380 and A400M critical on-board software,
scale development. The survey uncovered the and for the secondary flying command system of the
importance of producing tools that merit commercial A340 aircraft.
applications and that future tools should address
practical issues such as providing multi-language SCADE consists of 1. a Graphical editor 2. Simulator 3.
support, porting to a variety of platforms, version a Code generator that automatically translate graphical
control, and assistance for co-operative working by specification into C code 4. a model checker [3]. Esterel
multiple engineers on single developments. Increased Technologies, reported that SCADE significantly
automation was also suggested, and that proof tools need decreased the number of coding errors during the
to be incorporated in other tools used for analysis, development of Airbus’s DO-178B Level A Controllers
testing and design and the overall development for the A340 series aircraft.
environment. The paper reveals that there is not enough
to support the relationship between the adoption of Another research paper, reports that Airbus has used
formal verification methods and reduction in overall formal methods for years to specify avionics systems.
development cost. These methods have helped Airbus to significantly
shorted development cycles of their flight control
The final part of his paper presents the Verified Software systems especially the automatic generation of code
Repository. Initially proposed by Hoare in 2003, as a from formal specification tool SCADE. The first project
challenge for the computer science community to that Airbus in collaboration with ONERA was launched
develop a verifying compiler, it, over the years morphed to prove that the use of formal techniques based on
into a challenge to develop a Verified Software SCADE language and SCADE Design Verifier for
Repository which would contain hundreds of programs specifying avionic systems yields positive results.
SCADE which uses on graphical dataflow synchronous REFERENCES
language, divides time into discrete instants by a global
clock. The synchronous program reads inputs from [1] J. Woodcock, P. G. Larsen, J. Bicarregui, and J.
external environment and computes the output. Fitzgerald, “Formal methods,” ACM Computing
Surveys, vol. 41, no. 4, pp. 1–36, Jan. 2009.
Formal verification of properties is achieved by
expressing the properties derived from system [2] R. J. Punnoose, R. C. Armstrong, M. H. Wong, and
requirements and formalization and later expressed in M. Jackson, “Survey of Existing Tools for Formal
SCADE using synchronous observer techniques. The Verification.,” Jan. 2014.
process begins with property P and system S and
hypothesis H. What is required is proof that P is satisfied [3] T. Bochot, P. Virelizier, H. Waeselynck, and V.
by S under a set of H. To the designer builds a System S’ Wiels, “Model checking flight control systems: The
(S prime); the verification is required to prove that the Airbus experience,” 2009 31st International
output of system s’ is true. Conference on Software Engineering - Companion
Volume, 2009.
The SCADE Designer Verifier tool aims to prove that
the property is proved, otherwise a counter example that [4] G. Durrieu, O. Laurent, C. Seguin, and V. Wiels,
falsifies the property is generated. If property could not “Formal Proof and Test Case Generation for Critical
be proved, then it will display the results as Embedded Systems Using Scade,” Building the
indeterminate, neither true nor false. [4] Information Society IFIP International Federation for
Information Processing, pp. 499–504.

View publication stats