# Presentation: 253209

## From Informal Safety-Critical Requirements   to Property-Driven Formal Validation

- Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta
- Fondazione Bruno Kessler
-  Istituto per la Ricerca Scientifica e Tecnologica

- LFM 2008

- April 30, 2008

## Outline

- Requirements Analysis
- Requirements engineering
- Requirements specification
- Requirements formal validation
- Goals of the project
- The proposed methodology
- Informal analysis
- Formalization
- Formal validation
- Conclusions and future directions

- LFM 2008

- April 30, 2008

## Requirement Analysis

- LFM 2008

- April 30, 2008

## Requirements definition

- Set of properties that describe the system under development
- Configurations
- Entities
- Relationships
- Behaviors
- What is admissible
- What must not happen
- Requirements analysis is a pervasive problem in nowadays industry

- LFM 2008

- April 30, 2008

## Requirements engineering

- Definitions of
- Goals
- Scenarios
- Models
- Misuse cases
- Analysis mainly based on inspection
- Important for analysis of functional, quality, and security requirements
- High cost of flaws in the safety-critical specification
- Formal methods must be integrated

- LFM 2008

- April 30, 2008

## Requirements Specification

- Natural language is widely used as specification language
- ambiguous
- hard to process automatically
- statistical natural language processing
- controlled natural language
- requires background information
- knowledge representation, taxonomies
- Formal languages are often too difficult
- Important modeling issues
- modeling real-time and space
- not only discrete data
- hybrid automata as semantic model
- modeling class/instance relationship
- modeling temporal evolution

- LFM 2008

- April 30, 2008

## Formal languages for requirements

- Logic is usually used as language for property specification
- Examples: FOL, LTL, CTL, DL, ...
- In hardware design, standards for languages to represent of properties and design intent are emerging (e.g. PSL, SVA)
- Requirement → formula is usually a one-to-one mapping
- Every property/formula defines what is admissible
- Opposite to model specification
- System represented by abstract machines
- Examples: Automata, Petri Nets, Z, B, VDM, CCS, ...
- Notably: SCR
- used for requirement analysis
- the set of formulas define an abstract machine

- LFM 2008

- April 30, 2008

## Formal Verification Methods

- Theorem Proving
- general and expressive language
- both system and properties expressed in the same language
- not automatic
- Model Checking
- more restricted language
- system as finite state automaton
- properties as temporal logic formulae
- more effective engine
- based on search
- complete answer
- yes, system is correct
- no, here is a counterexample

- LFM 2008

- April 30, 2008

## Requirements formal validation

- Standard verification setting:
- the design is under analysis
- the requirements are taken as “golden”
- verification means checking compliance
- system has no behavior violating requirements
- New focus: requirements, not model
- There is no model (yet)
- Here the goal is to enhance quality of requirements
- No clear definition of correctness
- Several ways in which requirements might be flawed
- inconsistent (contradictory)
- too strict (some desired behaviors are not possible)
- too weak (some undesired behaviors are admissible)
- unrealizable (system would have to foresee the future to be implemented)

- LFM 2008

- April 30, 2008

## Goals of the project

- LFM 2008

- April 30, 2008

## Methodology goals

- Validation of natural language requirements
- Bridging the gap between natural language and formal analysis
- Enhancing the quality of the requirements
- Increasing the confidence in their correctness

- LFM 2008

- April 30, 2008

## Methodology Desiderata

- Usability
- Avoid intricate formalisms
- Hide formal methods with semiformal representations
- Formalization close to the original specification
- Traceability
- Link between one requirement and formal counterpart
- Automation of the verification process
- Validation applicable to parts of the specification
- Hierarchical approach
- Modular approach
- Incremental approach
- What-if analysis

- LFM 2008

- April 30, 2008

## Main issues

- Human factor in formalization
- Expressiveness of the formal language
- Completeness of validation
- Quality of feedback
- Complexity of the verification

- LFM 2008

- April 30, 2008

## ETCS case study

- Specification for the interoperability between train on-board and track-side systems.
- Complex, huge set of requirements
- Very ambiguous natural language
- NL cannot be substituted
- Mixed components functionalities
- Global properties
- Optional functionalities of components

- LFM 2008

- April 30, 2008

## New Methodology

- LFM 2008

- April 30, 2008

## Overview

- Step 1: Informal analysis
- Step 2: Formalization
- Step 3: Formal analysis

- LFM 2008

- April 30, 2008

## Step 1: Informal Analysis

- Supported by standard RE tools
- Standard checklist-based analysis to support the formalization
- Requirements Identification
- Requirements Categorization
- Customized taxonomy
- Definitions
- Properties (invariants, restrictions)
- Functionalities
- Procedures
- Scenarios
- Requirements Structure
- Define relationships among requirements
- Dependency links (A → B)
- Conflict links (A → not B)
- Requirements Quality
- Relevant, verifiable, ...
- Requirements Status
- Formalized, validated, to be disambiguated, ...

- LFM 2008

- April 30, 2008

## Step 2: Formalization

- Unified Modeling Language
- de facto standard in model based design
- common in software engineering
- wide tool support
- (semi-)formal
- very rich
- unclear semantics
- We propose a restricted use of UML
- clear semantics
- different diagrams depending on classifications of natural language
- We extend UML with Controlled Natural Language
- Highly-restricted syntax
- Express invariants and temporal behaviors

- LFM 2008

- April 30, 2008

## Proposed Specification Language

- Class diagrams (glossary/ontology)
- Classes
- Attributes
- Associations
- Inheritance relationships
- Methods
- State machines (procedures)
- States
- Transitions (event [guard]/transition)
- Sequence diagrams (scenarios)
- Timeline
- Methods calls
- Constraints (assumptions on system and environment behaviors)
- Property specification language
- Predicates over the UML model
- First-order terms
- Quantifiers over the class universe

- LFM 2008

- April 30, 2008

## Examples – class

*“**For each section composing the MA the following information shall be given;*
*a) Length of the section*
*b) Optionally, Section time-out value and distance from beginning of section to Section Time-out stop location”*

- Movement authority

- Section

- Length

- Distance

- ....

- ....

- INVAR
- Distance=Beginning_location-
- Timeout_stop_location

- 1..n

- Timeout

- Timeout_stop_location

- Beginning_location

- LFM 2008

- April 30, 2008

## Example – State Machine

- “*Each procedure is defined by a set of mandatory requirements and/or by a state transition chart (where convenient).*”

- LFM 2008

- April 30, 2008

## Example - Constraints

- “*A Balise Group is linked when its linking information is known in advance*”

- Onboard

- Balise_Group

- Linked

- Linking_info

- ....

- ....

- BEHAVIOR  always
- (if onboard.Receive_linking_info=linking_info
-  then linked=true until Location=onboard.position)

- Location

- Location

- Received_linking_info

- LFM 2008

- April 30, 2008

## Step 3: Formal Analysis

- Main checks:
- Consistency
- Scenarios
- Properties
- Realizability
- Consistency checking
- Is there a configuration and an evolution thereof consistent with the specification?
- Scenario checking
- Is there a configuration and an evolution thereof consistent with the specification and a given scenario?
- Property checking
- Is there a configuration and an evolution thereof consistent with the specification and a violation of the property?
- Realizability
- Is there an implementation that realizes the specification?

- LFM 2008

- April 30, 2008

## Verification procedure

- Definition of the verification domain
- User defined
- Finite recursion
- Small domain encoding
- Symbolic encoding
- Semantic model: fair infinite-state transition systems with temporal constraints
- Space minimization based on invariants
- Abstraction-based verification (CEGAR)
- Automatic abstraction with SMT and BDD
- Model checking with BDDs or SAT
- Automatic refinement with interpolation
- Tools: NuSMV, MathSAT
- Boolean abstraction of temporal formulas

- LFM 2008

- April 30, 2008

## Step 3: Feedback

- Traces
- Witnesses in case of consistency
- Counterexample in case of property violation
- Unsat cores
- Minimal inconsistent subset
- Vacuity
- Irrelevant sub-formulas of the property
- Presentation of results
- Sequence of method calls (sequence diagrams)
- Tree of event combinations (fault-tree analysis)

- LFM 2008

- April 30, 2008

## Conclusions and future work

- The methodology accomplishes the goal
- Usability
- Traceability
- Automation
- Feedback
- Ongoing feasibility study
- Ongoing development of tool support
- RSA plug-in to interact with ReqPro
- RSA plug-in to support formalization
- RSA plug-in with NuSMV back-end
- Many open research directions
- Controlled natural language
- Automatic instanciation
- Infinite domain
- Generalize CEGAR

## References

- Requirements validation
- Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta: Boolean Abstraction for Temporal Logic Satisfiability. CAV 2007
- Alessandro Cimatti, Marco Roveri, Stefano Tonetta: Syntactic Optimizations for PSL Verification. TACAS 2007
- Ariel Fuxman, Lin Liu, John Mylopoulos, Marco Roveri, Paolo Traverso: Specifying and analyzing early requirements in Tropos. Requir. Eng. 9(2): 132-150 (2004)
- Ingo Pill, Simone Semprini, Roberto Cavada, Marco Roveri, Roderick Bloem, Alessandro Cimatti: Formal analysis of hardware requirements. DAC 2006
- Realizability
- Nir Piterman, Amir Pnueli, Yaniv Sa'ar: Synthesis of Reactive(1) Designs. VMCAI 2006
- Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev: Diagnostic Information for Realizability. VMCAI 2007
- Fault-tree analysis
- Richard Banach, Marco Bozzano: Retrenchment, and the Generation of Fault Trees for Static, Dynamic and Cyclic Systems. SAFECOMP 2006
- Piergiorgio Bertoli, Marco Bozzano, Alessandro Cimatti: A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis. MoChArt 2006
- Marco Bozzano, Adolfo Villafiorita: The FSAP/NuSMV-SA Safety Analysis Platform. STTT 9(1): 5-24 (2007)
- Vacuity
- Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh: Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18(2): 141-163 (2001)
- Doron Bustan, A. Flaisher, Orna Grumberg, Orna Kupferman, Moshe Vardi: Regular Vacuity. CHARME 2005
- Controlled Natural Language
- Schwitter: English as a Formal Specification Language. DEXA 2002
- Nelken, Francez: Automatic Translation of Natural Language Specification Systems into Temporal Logic. CAV 1996

- LFM 2008

- April 30, 2008