scholarly journals A Driver’s License Test for Driverless Vehicles

2017 ◽  
Vol 139 (12) ◽  
pp. S13-S16 ◽  
Author(s):  
Houssam Abbas ◽  
Matthew E. O’Kelly ◽  
Alena Rodionova ◽  
Rahul Mangharam
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Autonomous Vehicle ◽  
Reachability Analysis ◽  
Initial State ◽  
Left Turn ◽  
Interactive Technique ◽  
Driver's License

This article elaborates the approaches that can be used to verify an autonomous vehicle (AV) before giving it a driver’s license. Formal methods applied to the problem of AV verification include theorem proving, reachability analysis, synthesis, and maneuver design. Theorem proving is an interactive technique in which the computer is largely responsible for demonstrating that the model satisfies the specification, with occasional help from the user. The latter provides lemmas and axioms that the tool leverages to advance the proof towards its conclusion. Reachability analysis is used to verify the operation of the AV during navigation. This provides an extension of onboard diagnostics to whole-AV operation, where the diagnosis does not concern one component’s requirements, but the safety of the entire AV. Another approach is to design correct-by-construction controllers from preverified maneuvers. The basic idea is that one builds a library of maneuvers, such as Left-Turn and Right-Turn, and verifies that the car can perform these maneuvers from any initial state.

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.

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.

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.

scholarly journals Space Debris Collision Detection using Reachability

10.29007/5313 ◽  
2018 ◽  
Author(s):  
Kerianne Hobbs ◽  
Peter Heidlauf ◽  
Alexander Collins ◽  
Stanley Bak
Keyword(s):  
Collision Detection ◽  
Space Debris ◽  
Reachability Analysis ◽  
Problem Structure ◽  
Initial State ◽  
Time Step ◽  
Variable Size ◽  
Abstraction Refinement ◽  
Counter Example ◽  
State Uncertainty

Benchmark Proposal: Space debris tracking and collision prediction is a growing world- wide problem as more and more objects are placed into orbit. While traditional methods simulate particles with Gaussian uncertainty to make collision predictions, we instead ana- lyze the problem from a reachability perspective. The problem appears to require methods capable of quickly analyzing high-dimensional nonlinear systems, but we take advantage multiple kinds of problem structure to show that reachability analysis may be viable for this problem. In particular we present an initial analysis approach that uses numerical simulation for reachability analysis, and interval arithmetic with AABB trees for fast col- lision detection. The analysis uses a variable size time step with a counter-example guided abstraction refinement (CEGAR) method to increase analysis speed without sacrificing accuracy. Our approach can analyze upwards of thousands of orbiting objects faster than real-time, where each object is subject to some initial state uncertainty.

scholarly journals Conflicts, Models and Heuristics for Quantifier Instantiation in SMT

10.29007/jmd3 ◽  
2018 ◽  
Author(s):  
Andrew Reynolds
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Software Verification ◽  
Satisfiability Modulo Theories ◽  
Smt Solvers ◽  
Recent Advances ◽  
Common Technique ◽  
Quantifier Instantiation ◽  
Future Work

Satisfiability Modulo Theories (SMT) solvers have emerged as prominent tools in formal methods applications. While originally targeted towards quantifier-free inputs, SMT solvers are now often used for handling quantified formulas in automated theorem proving and software verification applications. The most common technique for handling quantified formulas in modern SMT solvers in quantifier instantiation. This paper gives an overview of recent advances in quantifier instantiation in SMT. In addition to the well-known technique known as E-matching, we discuss the use of conflicts and models for accelerating the search for (un)satisfiably. We further mention new instantiation-based techniques that are specialized to background theories such as linear real and integer arithmetic, and future work in this direction.

Cryptographic Protocol Verification Based on the Extension Rule

2014 ◽  
Vol 644-650 ◽  
pp. 3181-3184
Author(s):  
Hai Lin
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Formal Method ◽  
Cryptographic Protocols ◽  
Strong Sense ◽  
Protocol Verification ◽  
Cryptographic Protocol ◽  
Effective Technique ◽  
Extension Rule

The design of cryptographic protocols is error-prone. People have found serious security flaws in major cryptographic protocols. In recent years, people use formal methods to guarantee the correctness of cryptographic protocols in a strong sense. Resolution-based theorem proving is a widely-used formal method, but there are other techniques as well. For example, the extension rule is another technique used to prove things formally. In this paper, we propose to prove the correctness of cryptographic protocols based on the extension rule. We show that this is an effective technique, which can help to find the security flaws in major cryptographic protocols.

scholarly journals Simulation-Based Evaluation of Variation in Left-Turn Paths in the Coordinated Intersection Management

2021 ◽  
Vol 2021 ◽  
pp. 1-14
Author(s):  
Menglin Yang ◽  
Hao Yu ◽  
Lu Bai
Keyword(s):  
Autonomous Vehicle ◽  
Safety Level ◽  
Left Turn ◽  
Intersection Area ◽  
Vehicle Delay ◽  
Intersection Operation ◽  
Automation Control ◽  
Conflict Risk ◽  
Nominal Performance ◽  
Intersection Management

Coordinated intersection management (CIM) has gained more attention with the advance of connected and autonomous vehicle technology. The optimization of passing schedules and conflict separation between conflicting vehicles are usually conducted based on the predefined travelling paths through the intersection area in the CIM. In real-world implementation, however, the diversity of turn paths exists due to multiple factors such as various vehicle sizes and automation control algorithms. The aim of this paper is to investigate how the variation in left-turn paths affects the feasibility and viability of optimal passing schedules, as well as the safety and efficiency of intersection operation. To do this, we start with identifying six typical left-turn paths to represent the variation. A scenario-based simulation is first conducted by using each of the paths as the nominal path. The optimal schedules and the corresponding alternative schedules are generated to calculate indicators for nominal performance, average performance, and robustness. The best path is selected in terms of schedule optimality and robustness. With schedules obtained by solving CIM models using the selected path, the left-turning CAVs are assumed to travel along one of the six paths randomly to simulate the path divergence. A surrogate safety measure, PET, is utilized to assess the safety of the intersection under CIM. The theoretical PET with the nominal path and the actual PET with the random path are calculated for each conflict event. Comparisons of two PET sets show the increase in conflict risk and vehicle delay. The conclusion can be drawn that the variation in left-turn paths causes the decline in safety level and travelling efficiency and should be considered in the CIM model to ensure safe and efficient implementation in the intersection.

Sign in / Sign up

Export Citation Format

Share Document