Group Members

Muhammad Usman 044

Muhammad Nisar 035
Muhammad Ali 040
Presentation Topic
State Of The Art In The Research Of Formal
Verification
Abstract
• In recent years research in formal verification of hardware and software
has reached important progresses in the development of
methodologies and tools to meet the increasing complexity of systems.
The explicit role of Formal Verification is to find errors and to improve
the reliability on the accuracy of system design, which implies a
challenge for software engineering of this century. The purpose of this
research is to perform a systematic review of the literature to establish
the state of the art of research in formal verification during the last 10
years and to identify the approaches, methods, techniques and
methodologies used, as well as the intensity of those research activities.
Introduction
• Functional verification has become the bottleneck
for the design of complex systems. Simulating
designs is money-demanding and time-demanding
and performing a complete simulation is almost
impossible. Currently, as a solution for these
problems, designers have started using formal
methods to perform formal verification on most of
products. But there is still a wide gap for the
verification of big designs, which can be built but
cannot be verified completely because of the
complexity of the problems they deal with.
Introduction cont
• This has caused that in many countries,
the academic world, industry and
governments must face the challenge of
reducing this technological gap and
proposing new and ingenious solutions for
specifying, designing, structuring and
applying test cases by using formal
verification
Introduction cont
• Formal verification is a crucial element in
the development of the current complex
information systems. Moore’s Law is still
applied to determine the growth rate of
the complexity of software and hardware
products, but the complexity of
verification becomes more complicated
Introduction cont
• Formal verification (FV) is a systematic process that
uses mathematical reasoning to verify that design
specification remains the same during
implementation. With this verification is possible to
overcome the challenges of simulation because all
the possible input values can be explored
algorithmically or thoroughly. In other words, to
achieve a high degree of observation of the product
it is not necessary to exaggerate the design or
creating multiple scenarios.
Introduction cont
• One of the objectives of FV is to guarantee the complete
coverage of the space of the states in the tested design,
to achieve that it uses and applies techniques like model
verification through the investigation of space of states
and automated techniques to demonstrate the
theorems. Currently, the most automated and most
accepted FV technique is Symbolic Model Verifier or SMV
and, despite its success as an important method for the
formal verification of sequential commercial designs, is
still limited in relation to the size of the verifiable designs
Introduction cont
• Formal verification requires that engineers think different.
For instance, simulation is empirical, this means that using
trial and error to test all of the possible combinations and
try to discover errors can take significant time. For this
reason, it does not fully achieve it. Besides, because
engineers must define and create a high number of input
scenarios, they focus their efforts on breaking the design
but not on which design must do. Formal verification, on
the conflicting, is mathematical and exhaustive and allows
engineers become focused exclusively in finding which one
is the correct behavior of the design
Formal Methods
• Formal methods are system design
techniques that use rigorously specified
mathematical models to build software and
hardware systems. In contrast to other
design systems, formal methods use
mathematical proof as a complement to
system testing in order to ensure correct
behavior.
Formal Method In Software Engineering

• In software engineering, formal methods are

mathematical approaches to solving software
(and hardware) problems at the requirements,
specification, and design levels. Formal
methods are most likely to be applied to
safety-critical or security-critical software and
systems, such as Pharmaceutical industry
software.
 Formal Verification
• Formal verification (FV) is a systematic
process that uses mathematical reasoning
to verify that design specification remains
the same during implementation. With
this verification is possible to overcome
the challenges of simulation because all
the possible input values can be explored
algorithmically.
 Role Of Formal Verification
• The explicit role of Formal Verification is to find errors
and to improve the reliability on the accuracy of
system design, which implies a challenge for software
engineering of this century. The purpose of this
research is to perform a systematic review of the
literature to establish the state of the art of research
in formal verification during the last 10 years and to
identify the approaches, methods, techniques and
methodologies used, as well as the strength of those
research activities.
Methodological Process

• Performing a systematic review to

literature can be divided in three main
stages:-
(1) Planning
(2) Execution
(3) Documentation
Methodological Process
Stages Procedures
Specifying research questions
Planning Developing the review protocol
Validating the review protocol
Identifing relevant research
Selecting primary studies
Execution Assesing the quality of studies
Extracting required data
Producing data
Writing the review report
Documentation
Validating the report
• 1. The research questions
• 2. The searching process
• 3. The inclusion and exclusion criteria
• 4. Quality assessment
• 5. Data collection
• 6. Data analysis
Research questions
• Research questions The research questions applied during the
development of this research were:
• Q1: In which fields of formal verification is conducted
research currently?
• Q2: Which application methodology is the most researched?
• Q3: In which formal verification technique is conducted
research more frequently?
• Q4: Which approach and research method is the most used?
• Q5: Which is the intensity of research activities in formal
verification?
Research Answer
• Q:1) Discret mathematical, declarative language, formal language, formal
method, formal specification and formal verification: in the abstract or in
the content.
• Q:2) Experimentation, case study, stochastic and experimental: in the
abstract or in the content.
• Q:3) Peer, animation, simulation, agile methods and XP: in the abstract or in
the content.
• Q:4) The observation of the results for Q1, Q2 y Q3 permitted classifying
the approach and the research method for Q4. For the empirical research it
was performed a search of terms experiment, survey, case study, empirical
research in the abstract and within the content.
• Q:5) Formal verification AND research: in the title and combined with each
year of the timeline. For Q5.
Research process
• A systematic review about a specific subject must identify and
highlight the specific sources about of the object of study;
however; in the field of formal verification were not found that
sources, because the related studies can be published in
journals and conferences related to both functional verification
and formal methods. The purpose of the search was to identify
the primary studies which could be included or excluded from
the definitive set of studies of the review. The plan involved an
automated search in the ACM Digital Library, IEEE Digital
Library, Science Direct and Springer Link, based on the timeline
between January 2000 and April 2011.
Quality assessment
• The purpose of this stage is to validate the
fact that the primary studies selected exhibit
solidity regarding methodology and results.
Considering the high standards of the review
process performed by the selected journals
and databases, it was concluded, based on
the evidences that the primary studies
selected exhibit good quality.
Data collection
• After finishing the inclusion or exclusion process, the set of data of the primary studies was structured.
During this stage the following attributes were collected:
• 1. Type of event: journal, conference-congress, workshop.
• 2. Published in: journal, proceedings.
• 3. Publishing house: ACM, IEEE, Springer, Elsevier.
• 4. Year of publishing: 2000 to 2011 timeline.
• 5. Country.
• 6. Classification of the approach and method. According to Glass et al. (2002), the main research and
scientific approaches are: descriptive, explanatory and empirical and, according to Wohlin et al. (2000)
and Dyba and Dingsoyr (2008), there are three methods of research used to evaluate techniques,
methods and tools: survey, case study and experiment.
• 7. Classification of the field. The selected fields for the research were: mathematical models, formal
languages, automated models, declarative languages, formal methods and formal specification.
• 8. Classification of the methodology. The analyzed methodologies were: experimentation, case study,
stochastic and heuristics.
• 9. Classification of the technique. The selected primary studies were classified according to the
treatment
Data collection
• • Technological and scientific research article. Document that
presents in a detailed manner the original results of finished research
projects. Their structure generally has four sections: introduction,
methodology, results and conclusions.
• • Reflection article. Document that presents the results of finished
research from an analytic, critical or interpretative point of view
about a specific topic and considering original sources.
• • Review article. Document which analyzes systematizes and
integrates the results of published or nonpublished research about a
science or technology field, having as purpose disseminating the
advances and trends of development. A characteristic feature is that
they present a detailed bibliographic review of, at least, 50 references
 Conclusion And future work
• The objective of this work was to summarize the state of the art about
the scientific research in the field of formal verification and in order to
achieve that a systematic review of the literature was performed,
considered like the first step in the research paradigm based in
evidence. FV has lately become a practical mean for detecting the
presence of unwanted behaviors in software products, a required
feature for critical models. The models for checking quality in the
software industry and those used by the testers of advanced theorems,
make easier performing complex analysis of specifications in an
automated or semi-automated way.
conclusion
• Because of the nature of formal verification, the most
representative research approach is the empirical,
due in part to the need of checking in a case study the
model created through observation and result
analysis. The research articles included in this study
cover a wide variety of topics related to FV, like Petri
Nets for control devices, digital circuits and processors
in which they are used to perform exhaustive
verification processes in order to optimize the design;
the temporal logic
conclusion
• to verify formally the concurrence of access to the control
algorithms and the security specifications of information systems to
ensure their security; formal semantics for business specifications;
the verification of system requirements; the analysis of hierarchical
processor, which divides into a set of conditions for the
achievement of a simpler verification for reasoning, allowing to
perform the test in the different architecture levels; the heuristic
ones to formally and automatically verify complex systems like the
next generations of microprocessors. Software engineering is facing
up a permanent challenge with formal verification, because its goal
is to reduce the gap between high-complexity systems and the
applicability of good practices in the whole design process.
Thank
You