Formal Specification and Model Checking of a Ride-sharing System in Maude

2020 ◽  
pp. 187-204
Author(s):  
Eiichi Muramoto ◽  
Kazuhiro Ogata ◽  
Yoichi Shinoda
Keyword(s):  
Model Checking ◽  
Formal Specification ◽  
Ride Sharing

A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA*

2020 ◽  
Vol 30 (10) ◽  
pp. 1481-1523
Author(s):  
Kazuhiro Ogata
Keyword(s):  
Model Checking ◽  
Shortest Path ◽  
Formal Specification ◽  
Model Check ◽  
Shortest Paths ◽  
Path Finding ◽  
Property A ◽  
Goal Node ◽  
The Cost ◽  
Start Node

The paper describes how to formally specify three path finding algorithms in Maude, a rewriting logic-based programming/specification language, and how to model check if they enjoy desired properties with the Maude LTL model checker. The three algorithms are Dijkstra Shortest Path Finding Algorithm (DA), A* Algorithm and LPA* Algorithm. One desired property is that the algorithms always find the shortest path. To this end, we use a path finding algorithm (BFS) based on breadth-first search. BFS finds all paths from a start node to a goal node and the set of all shortest paths is extracted. We check if the path found by each algorithm is included in the set of all shortest paths for the property. A* is an extension of DA in that for each node [Formula: see text] an estimation [Formula: see text] of the distance to the goal node from [Formula: see text] is used and LPA* is an incremental version of A*. It is known that if [Formula: see text] is admissible, A* always finds the shortest path. We have found a possible relaxed sufficient condition. The relaxed condition is that there exists the shortest path such that for each node [Formula: see text] except for the start node on the path [Formula: see text] plus the cost to [Formula: see text] from the start node is less than the cost of any non-shortest path to the goal from the start. We informally justify the relaxed condition. For LPA*, if the relaxed condition holds in each updated version of a graph concerned including the initial graph, the shortest path is constructed. Based on the three case studies for DA, A* and LPA*, we summarize the formal specification and model checking techniques used as a generic approach to formal specification and model checking of path finding algorithms.

scholarly journals Logic-based specification and verification of homogeneous dynamic multi-agent systems

2020 ◽  
Vol 34 (2) ◽  
Author(s):  
Riccardo De Masellis ◽  
Valentin Goranko
Keyword(s):  
Normal Form ◽  
Model Checking ◽  
Formal Specification ◽  
Formal Semantics ◽  
Fixed Number ◽  
State Transitions ◽  
Multi Agent Systems ◽  
Worst Case ◽  
Worst Case Complexity ◽  
Multi Agent

Abstract We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems. Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided into controllable (by the system supervisor/controller) and uncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic, where one can specify properties of the type “a coalition of (at least) n controllable agents can ensure against (at most) m uncontrollable agents that any possible evolution of the system satisfies a given objective $$\gamma$$ γ ″, where $$\gamma$$ γ is specified again as a formula of that language and each of n and m is either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic $${\mathcal {L}}_{\textsc {hdmas}}$$ L H D M A S and define normal form of its formulae. We then prove that every formula in $${\mathcal {L}}_{\textsc {hdmas}}$$ L H D M A S is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example.

Formal Modeling and Verification of Security Property in Handel C Program

2012 ◽  
Vol 3 (3) ◽  
pp. 50-65
Author(s):  
Yujian Fu ◽  
Jeffery Kulick ◽  
Lok K. Yan ◽  
Steven Drager
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Formal Specification ◽  
Critical Systems ◽  
Formal Approach ◽  
C Programs ◽  
Translation Rule ◽  
Security Properties ◽  
C Program ◽  
Security Property

Multi-million gate system-on-chip (SoC) designs easily fit into today’s Field Programmable Gate Arrays (FPGAs). As FPGAs become more common in safety-critical and mission-critical systems, researchers and designers require information flow guarantees for the FPGAs. Tools for designing a secure system of chips (SOCs) using FPGAs and new techniques to manage and analyze the security properties precisely are desirable. In this work we propose a formal approach to model, analyze and verify a typical set of security properties – noninterference – of Handel C programs using Petri Nets and model checking. This paper presents a method to model Handel C programs using Predicate Transition Nets, a type of Petri Net, and define security properties on the model, plus a verification approach where security properties are checked. Three steps are used. First, a formal specification on the Handel C description using Petri Nets is extracted. Second, the dynamic noninterference properties with respect to the Handel C program statements are defined on the model. To assist in verification, a translation rule from the Petri Nets specification to the Maude programming language is also defined. Thus, the formal specification can be verified against the system properties using model checking. A case study of the pipeline multiplier is discussed to illustrate the concept and validate the approach.

scholarly journals Integrating formal specifications into applications: the ProB Java API

2020 ◽  
Author(s):  
Philipp Körner ◽  
Jens Bendisposto ◽  
Jannik Dunkelau ◽  
Sebastian Krings ◽  
Michael Leuschel
Keyword(s):  
Model Checking ◽  
Case Studies ◽  
Formal Specification ◽  
Formal Specifications ◽  
Formal Models ◽  
Model Checker ◽  
Enabling Technology ◽  
Code Generators ◽  
Proof Techniques ◽  
The Common

Abstract The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the ProB animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.

Tendermint Blockchain Synchronization: Formal Specification and Model Checking

2020 ◽  
pp. 471-488
Author(s):  
Sean Braithwaite ◽  
Ethan Buchman ◽  
Igor Konnov ◽  
Zarko Milosevic ◽  
Ilina Stoilkovska ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Specification
Sign in / Sign up

Export Citation Format

Share Document