Autopilot Mode Transitions and Voter Logic Validation Using Model Checking: A Design Study of Formal Methods

2021 ◽  
pp. 263-281
Author(s):  
Ravi Kiran ◽  
Yogananda Jeppu
Keyword(s):  
Model Checking ◽  
Formal Methods ◽  
Design Study ◽  
Mode Transitions

A Formal Approach to the Verification of Adaptability Properties for Mobile Multimodal User Interfaces

2010 ◽  
pp. 53-74
Author(s):  
Nadjet Kamel ◽  
Sid Ahmed Selouani ◽  
Habib Hamam
Keyword(s):  
Life Cycle ◽  
Model Checking ◽  
Formal Methods ◽  
User Interfaces ◽  
Mobile Systems ◽  
Formal Approach ◽  
Transition Systems ◽  
Development Life Cycle ◽  
Fully Automatic ◽  
Multimodal User Interfaces

Multimodal User Interfaces (MUIs) offer to users the possibility to interact with systems using one or more modalities. In the context of mobile systems, this will increase the flexibility of interaction and will give the choice to use the most appropriate modality. These interfaces must satisfy usability properties to guarantee that users do not reject them. Within this context, we show the benefits of using formal methods for the specification and verification of multimodal user interfaces (MUIs) for mobile systems. We focus on the usability properties and specifically on the adaptability property. We show how transition systems can be used to model the MUI and temporal logics to specify usability properties. The verification is performed by using fully automatic model-checking technique. This technique allows the verification at earlier stages of the development life cycle which decreases the high costs involved by the maintenance of such systems.

Formal Verification Methods

2015 ◽  
pp. 10-20
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Formal Methods ◽  
Theorem Proving ◽  
Critical Systems ◽  
Verification Methods

This chapter provides a brief introduction to the domain of formal methods (Boca, Bowen, & Siddiqi, 2009) and the most commonly used verification methods (i.e., theorem proving [Harrison, 2009] and model checking [Baier & Katoen, 2008]). Due to their inherent precision, formal verification methods are increasingly being used in modeling and verifying safety and financial-critical systems these days.

The Role of Formal Methods in Software Development for Railway Applications

2014 ◽  
pp. 1103-1118
Author(s):  
Alessandro Fantechi
Keyword(s):  
Model Checking ◽  
Software Development ◽  
Formal Verification ◽  
Formal Methods ◽  
Industrial Application ◽  
Safety Certification ◽  
Software Designers ◽  
Recent Trends ◽  
Railway Domain

Formal methods for thirty years have promised to be the solution for the safety certification headaches of railway software designers. This chapter looks at the current industrial application of formal methods in the railway domain. After a recall of the dawning of formal methods in this domain, recent trends are presented that focus in particular on formal verification by means of model checking engines, with its potential and limitations. The paper ends with a perspective into the next future, in which formal methods will be expected to pervade in more respects the production of railway software and systems.

The Role of Formal Methods in Software Development for Railway Applications

2012 ◽  
pp. 282-297 ◽  
Author(s):  
Alessandro Fantechi
Keyword(s):  
Model Checking ◽  
Software Development ◽  
Formal Verification ◽  
Formal Methods ◽  
Industrial Application ◽  
Safety Certification ◽  
Software Designers ◽  
Recent Trends ◽  
Railway Domain

Formal methods for thirty years have promised to be the solution for the safety certification headaches of railway software designers. This chapter looks at the current industrial application of formal methods in the railway domain. After a recall of the dawning of formal methods in this domain, recent trends are presented that focus in particular on formal verification by means of model checking engines, with its potential and limitations. The paper ends with a perspective into the next future, in which formal methods will be expected to pervade in more respects the production of railway software and systems.

Observer Patterns for Timed Properties

2021 ◽  
Vol 9 (2) ◽  
pp. 1-17
Author(s):  
Djamila Baroudi ◽  
Safia Nait-Bahloul
Keyword(s):  
Model Checking ◽  
Embedded System ◽  
Formal Methods ◽  
Reachability Analysis ◽  
Domain Specific Language ◽  
Formal Specifications ◽  
Specific Language ◽  
Domain Specific ◽  
Formal Techniques ◽  
Timed Properties

Dwyer et al. proposed qualitative specification patterns that enable the practitioners of model checking tools to write formal specifications mainly used for automatic model checking. Although this involves formalisms that are not always easy to handle by engineers, to facilitate the integration of formal methods based on these definition patterns in the industrial field, several formal techniques and languages have been proposed. This paper studies a domain specific language named CDL which help non-experts writing formal specifications effortlessly. In CDL, a property is transformed into an observer automaton to perform a reachability analysis. The existing CDL patterns allow non-experts to reason about occurrence and order of events, but not enough about their timing. Furthermore, the semantics of patterns and transformations are not ideally formalized and are still complex. This work serves to extend the existing CDL system by patterns related to time. The contribution is illustrated in an industrial embedded system.

scholarly journals Let's Learn Their Language? A Case for Planning with Automata-Network Languages from Model Checking

2020 ◽  
Vol 34 (09) ◽  
pp. 13569-13575
Author(s):  
Jorg Hoffmann ◽  
Holger Hermanns ◽  
Michaela Klauck ◽  
Marcel Steinmetz ◽  
Erez Karpas ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Methods ◽  
Side Effect ◽  
The Other ◽  
Modeling Language ◽  
Ai Planning ◽  
Complex Environments ◽  
Exogenous Agents ◽  
Automata Network

It is widely known that AI planning and model checking are closely related. Compilations have been devised between various pairs of language fragments. What has barely been voiced yet, though, is the idea to let go of one's own modeling language, and use one from the other area instead. We advocate that idea here – to use automata-network languages from model checking instead of PDDL – motivated by modeling difficulties relating to planning agents surrounded by exogenous agents in complex environments. One could, of course, address this by designing additional extended planning languages. But one can also leverage decades of work on modeling in the formal methods community, creating potential for deep synergy and integration with their techniques as a side effect. We believe there's a case to be made for the latter, as one modeling alternative in planning among others.

Research on Hardware Design Verification Methods

2012 ◽  
Vol 588-589 ◽  
pp. 1208-1213
Author(s):  
Jie Zhang ◽  
Jian Qi ◽  
Yong Guan
Keyword(s):  
Model Checking ◽  
Formal Methods ◽  
Theorem Proving ◽  
Hardware Design ◽  
Equivalence Checking ◽  
Design Verification ◽  
Future Directions ◽  
Existing Problems ◽  
Verification Methods ◽  
Simulation Based

This paper first summarizes the existing basic theories and methods of hardware design verification. Then it analyzes and compares the simulation-based verification and formal methods-based verification, and discusses Equivalence Checking, Model Checking and Theorem Proving in detail. Finally, it points out the existing problems and the future directions in the field.

Towards a Wide Acceptance of Formal Methods to the Design of Safety Critical Software: an Approach Based on UML and Model Checking

2015 ◽  
pp. 612-627 ◽  
Author(s):  
Eduardo Rohde Eras ◽  
Luciana Brasil Rebelo dos Santos ◽  
Valdivino Alexandre de Santiago Júnior ◽  
Nandamudi Lankalapalli Vijaykumar
Keyword(s):  
Model Checking ◽  
Formal Methods ◽  
Safety Critical ◽  
Wide Acceptance

Guiding Simulation Model Verification by Model Checking

2010 ◽  
Vol 44-47 ◽  
pp. 3508-3513
Author(s):  
Wei Xia ◽  
Yi Ping Yao ◽  
Xiao Dong Mu ◽  
Fei Xing
Keyword(s):  
Model Checking ◽  
Simulation Model ◽  
Formal Methods ◽  
Important Determinant ◽  
Simulation Models ◽  
Systems Development ◽  
Model Verification ◽  
Model Driven ◽  
Simulation Speed ◽  
Simulation Systems

The accuracy and credibility of model is the most important determinant of development of Modeling and Simulation (M&S). There is a desperate need for an immediate practical solution to the problem of VV&A (Validation, Verification and Accreditation) of simulation systems. A discussion and experiment of the relative merits of informal methods and formal methods are provided in this paper. In spite of increasing simulation speed via parallelization, the number of problem cases that can be covered is not highly increased. On the other hand, formal methods have proven to be valuable techniques, but they require detailed specifications of systems and requirements, therefore they are not very accessible in practical simulation systems development. According to the exhaustiveness of formal methods, a Model Driven Architecture (MDA) based simulation VV&A framework guided by model checking is presented in this paper. This framework combines scalability of simulation with exhaustiveness of formal methods in order to get the best of both worlds for simulation model verification. It can provide more confidence in simulation models and increase the use of formal methods in the context of M&S by people that are not trained in formal techniques.

scholarly journals Mission Accomplished: An Introduction to Formal Methods in Mobile Robot Motion Planning and Control

2014 ◽  
Vol 02 (02) ◽  
pp. 201-216 ◽  
Author(s):  
Hai Lin
Keyword(s):  
Model Checking ◽  
Mobile Robot ◽  
Motion Planning ◽  
Formal Methods ◽  
Temporal Logic ◽  
Controller Design ◽  
Research Area ◽  
Natural Languages ◽  
High Level ◽  
Logic Model Checking

A new trend in the robotic motion planning literature is to use formal methods, like model checking, reactive synthesis and supervisory control theory, to automatically design controllers that drive a mobile robot to accomplish some high level missions in a guaranteed manner. This is also known as the correct-by-construction method. The high level missions are usually specified as temporal logics, particularly as linear temporal logic formulas, due to their similarity to human natural languages. This paper provides a brief overview of the recent developments in this newly emerged research area. A number of fundamental topics, such as temporal logic, model checking, bisimulation quotient transition systems and reachability controller design are reviewed. Additionally, the key challenges and possible future directions in this area are briefly discussed with references given for further reading.

Sign in / Sign up

Export Citation Format

Share Document