Industrial Experience with Formal Verification (Industrielle Erfahrungen mit Formaler Verifikation)

2001 ◽  
Vol 43 (1) ◽  
Author(s):  
Michael Payer
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Equivalence Checking ◽  
Functional Equivalence ◽  
Design Environment ◽  
Popular Method ◽  
The Past ◽  
Formal Equivalence ◽  
Functional Simulation ◽  
Low Coverage

In recent years, Formal Verification has become an increasingly popular method to verify the functional equivalence of different design views. Just recently, designers also start to speak about Model Checking, a methodology that allows to analyze functional properties of a design. In the past both, equivalence checking and property checking, have been carried out with functional simulation; with today′s designs of several 100K or even Mio. gates this is not feasible anymore. The main reasons are the unsatisfactory runtime and the low coverage of this approach. In this paper, I will report experiences with Formal Equivalence Verification in an industrial design environment.

scholarly journals “Most of” leads to undecidability: Failure of adding frequencies to LTL

2021 ◽  
pp. 82-101
Author(s):  
Bartosz Bednarczyk ◽  
Jakub Michaliszyn
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Statistical Reasoning ◽  
First Order ◽  
High Interest ◽  
The Past ◽  
Influence Networks

AbstractLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that $$\sigma $$ σ is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

Verification of Plastic Interactive Systems

i-com ◽  
2015 ◽  
Vol 14 (3) ◽  
Author(s):  
Raquel Oliveira ◽  
Sophie Dupuy-Chessa ◽  
Gaëlle Calvary
Keyword(s):  
Power Plant ◽  
User Interfaces ◽  
Nuclear Power ◽  
Interactive Systems ◽  
System Model ◽  
Equivalence Checking ◽  
The Past ◽  
Different Levels ◽  
Formal Techniques

AbstractInteractive systems have largely evolved over the past years. Nowadays, different users can interact with systems on different devices and in different environments. The user interfaces (UIs) are expected to cope with such variety. Plastic UIs have the capacity to adapt to changes in their context of use while preserving usability. Such capability enhances UIs, however, it adds complexity on them. We propose an approach to verifying interactive systems considering this adaptation capability of the UIs. The approach applies two formal techniques: model checking, to the verification of properties over the system model, and equivalence checking, to compare different versions of a UI, thereby identifying different levels of UI equivalence. We apply the approach to a case study in the nuclear power plant domain in which several UI are analyzed, properties are verified, and the level of equivalence between them is demonstrated.

scholarly journals Fast equivalence -- checking for quantum circuits

2010 ◽  
Vol 10 (9&10) ◽  
pp. 721-734
Author(s):  
Shigeru Yamashita ◽  
Igor L. Markov
Keyword(s):  
Formal Verification ◽  
Quantum Algorithms ◽  
Quantum Circuits ◽  
Equivalence Checking ◽  
Sat Solvers ◽  
Reversible Circuits ◽  
Verification Tools ◽  
Verification Methodology ◽  
Verification Techniques ◽  
Factoring Algorithm

We perform formal verification of quantum circuits by integrating several techniques specialized to particular classes of circuits. Our verification methodology is based on the new notion of a reversible miter that allows one to leverage existing techniques for simplification of quantum circuits. For reversible circuits which arise as runtime bottlenecks of key quantum algorithms, we develop several verification techniques and empirically compare them. We also combine existing quantum verification tools with the use of SAT-solvers. Experiments with circuits for Shor's number-factoring algorithm, containing thousands of gates, show improvements in efficiency by four orders of magnitude.

scholarly journals Environmental impacts on the design and arts environment for industry 3.0 cotton roller ginning process

2021 ◽  
Vol 8 (1) ◽  
pp. 22-34
Author(s):  
Vijayan Gurumurthy Iyer
Keyword(s):  
Impact Assessment ◽  
Environmental Impacts ◽  
Sustainable Design ◽  
Research Work ◽  
Water Remediation ◽  
Design Environment ◽  
Hazardous Waste Management ◽  
The Past ◽  
Disease Impact

The past five decades have been characterised by passage of the environmental impact assessment (EIA) legislation dealing with the environment, including legislation on the control of land, air and water pollution, solid and hazardous waste management, resource conservation and recovery, and soil and ground water and surface water remediation. The aim of this research is to investigate and discuss coronavirus and byssinosis disease impact assessment. Sustainable development is the artistic idea that science and humanities must live and meet their needs without compromising the efficacy and efficiency of future generations to meet their own needs. Prediction and assessment of environmental impacts (effects) on the design and arts environment for industry 3.0 cotton roller ginning process is provided. Sustainable design and arts are discussed in this research work. EIA of conventional design and arts is also investigated. Sustainable design and arts environment for cotton ginning process is presented. The case study and check of strengthening of agricultural extension through sustainable entrepreneurship is discussed in this article.   Keywords: Agriculture, arts, cotton, design, environment, entrepreneurship, ginning, sustainability.

A Methodology for Automatic Formal Verification of Enterprise Architecture

2019 ◽  
Vol 10 (1) ◽  
pp. 1-19
Author(s):  
Eduard Babkin ◽  
Pavel Malyzhenkov ◽  
Marina Ivanova ◽  
Nikita Ponomarev
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Iterative Process ◽  
Enterprise Architecture ◽  
Description Language ◽  
Architecture Description Language ◽  
Business Modeling ◽  
Business Alignment ◽  
Architecture Description ◽  
Software Prototype

For over a decade, IT-business alignment has been ranked as a top-priority management concern, but there is little research on practical ways to achieve the alignment. EA development is a continuous iterative process, which implicitly ensures the achievement of a specific IT-business alignment level. Therefore, it is necessary to formalize the requirements for architecture and be able to automatically verify them. The authors propose a new methodology for detecting logical contradictions in enterprise architecture models based on a model checking approach adopted in the context of business modeling. In such a methodology, they use ArchiMate standard for a conceptual enterprise architecture description language which is fully aligned with TOGAF. The authors also offer several important verification queries and demonstrate practical applicability of their approach using a software prototype of the modeling tool which exploits MIT Alloy Analyzer model checking framework integrated with AchiMate Archi workbench.

scholarly journals System Level Formal Verification via Model Checking Driven Simulation

2013 ◽  
pp. 296-312 ◽  
Author(s):  
Toni Mancini ◽  
Federico Mari ◽  
Annalisa Massini ◽  
Igor Melatti ◽  
Fabio Merli ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
System Level

scholarly journals A symbolic model checking approach in formal verification of distributed systems

2019 ◽  
Vol 9 (1) ◽  
Author(s):  
Alireza Souri ◽  
Amir Masoud Rahmani ◽  
Nima Jafari Navimipour ◽  
Reza Rezaei
Keyword(s):  
Distributed Systems ◽  
Model Checking ◽  
Formal Verification ◽  
Symbolic Model Checking ◽  
Symbolic Model

Model Checking for SpaceWire Error Detection Module

2012 ◽  
Vol 241-244 ◽  
pp. 3020-3025
Author(s):  
Ling Ling Dong ◽  
Yong Guan ◽  
Xiao Juan Li ◽  
Zhi Ping Shi ◽  
Jie Zhang ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Error Detection ◽  
System Model ◽  
Linear Search ◽  
Kripke Structure ◽  
Mathematical Methods ◽  
Safety Critical ◽  
Correctness Of Programs

Considerable attention has been devoted to prove the correctness of programs. Formal verification overcomes the incompleteness by applying mathematical methods to verify a design. SpaceWire is a well known communication standard. For safety-critical applications an approach is needed to validate the completeness of SpareWire design. This paper addresses formal verification of SpareWire error detection module. The system model was constructed by Kripke structure, and the properties were presented by linear temporal logic (LTL). Compared the verification of LTL with CTL (branch temporal logic), LTL properties could improve the verification efficiency due to its linear search. The error priority was checked using simulation guided by model checking. After some properties were modified, all possible behaviors of the module satisfied the specification. This method realizes complete validation of the error detection module.

Sign in / Sign up

Export Citation Format

Share Document