scholarly journals Progress in Certifying Hardware Model Checking Results

2021 ◽  
pp. 363-386
Author(s):  
Emily Yu ◽  
Armin Biere ◽  
Keijo Heljanko
Keyword(s):  
Model Checking ◽  
Formal Framework ◽  
Proof Checker ◽  
The Given ◽  
Certification Method ◽  
Quantifier Alternation

AbstractWe present a formal framework to certify k-induction-based model checking results. The key idea is the notion of a k-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also present Certifaiger, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.

scholarly journals Dynamic Logic for Data-aware Systems: Decidability Results

2017 ◽  
Author(s):  
Francesco Belardinelli ◽  
Andreas Herzig
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
English Auctions ◽  
First Order ◽  
Formal Framework ◽  
Data Content ◽  
Order Extension

We introduce a first-order extension of dynamic logic (FO-DL), suitable to represent and reason about the behaviour of Data-aware Systems (DaS), which are systems whose data content is explicitly exhibited in the system’s description. We illustrate the expressivity of the formal framework by modelling English auctions as DaS, and by specifying relevant properties in FO-DL. Most importantly, we develop an abstraction-based verification procedure, thus proving that the model checking problem for DaS against FO-DL is actually decidable, provided some mild assumptions on the interpretationdomain.

scholarly journals Model Checking Temporal Logic Formulas Using Sticker Automata

2017 ◽  
Vol 2017 ◽  
pp. 1-33 ◽  
Author(s):  
Weijun Zhu ◽  
Changwei Feng ◽  
Huanmei Wu
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Complex Problem ◽  
Finite State Automaton ◽  
Dna Molecules ◽  
Single Stranded Dna ◽  
Finite State ◽  
Input Strings ◽  
Logic Model Checking ◽  
The Given

As an important complex problem, the temporal logic model checking problem is still far from being fully resolved under the circumstance of DNA computing, especially Computation Tree Logic (CTL), Interval Temporal Logic (ITL), and Projection Temporal Logic (PTL), because there is still a lack of approaches for DNA model checking. To address this challenge, a model checking method is proposed for checking the basic formulas in the above three temporal logic types with DNA molecules. First, one-type single-stranded DNA molecules are employed to encode the Finite State Automaton (FSA) model of the given basic formula so that a sticker automaton is obtained. On the other hand, other single-stranded DNA molecules are employed to encode the given system model so that the input strings of the sticker automaton are obtained. Next, a series of biochemical reactions are conducted between the above two types of single-stranded DNA molecules. It can then be decided whether the system satisfies the formula or not. As a result, we have developed a DNA-based approach for checking all the basic formulas of CTL, ITL, and PTL. The simulated results demonstrate the effectiveness of the new method.

scholarly journals Self-Adaptive Systems Planning with Model Checking using MAPE-K

2020 ◽  
Author(s):  
Aristóteles Esteves Marçal Da Silva ◽  
Aline Maria Santos Andrade ◽  
Sandro Santos Andrade
Keyword(s):  
Model Checking ◽  
Adaptive Systems ◽  
Traffic Monitoring ◽  
Self Healing ◽  
Reference Architecture ◽  
Systems Planning ◽  
Autonomous Planning ◽  
Formal Framework ◽  
Self Adaptive

This paper presents a model checking-based approach to support the autonomous planning of adaptation actions in Self-Adaptive Systems, designed in consonance with the MAPE-K reference architecture. We evaluated our approach with a case-study aiming at verifying self-healing and self-organizing properties in a distributed and decentralized traffic monitoring system. Results show that our approach is able to generate adaptation plans satisfying the goals for all expected scenarios in such a case-study, providing a flexible formal framework where adaptation strategies and goals can be inserted/removed.

scholarly journals Feature partitioning for robust tree ensembles and their certification in adversarial scenarios

2021 ◽  
Vol 2021 (1) ◽  
Author(s):  
Stefano Calzavara ◽  
Claudio Lucchese ◽  
Federico Marcuzzi ◽  
Salvatore Orlando
Keyword(s):  
Machine Learning ◽  
Machine Learning Algorithms ◽  
Brute Force ◽  
Accuracy Improvement ◽  
Safe Environment ◽  
Feature Partitioning ◽  
Feature Based ◽  
Brute Force Approach ◽  
The Given ◽  
Certification Method

AbstractMachine learning algorithms, however effective, are known to be vulnerable in adversarial scenarios where a malicious user may inject manipulated instances. In this work, we focus on evasion attacks, where a model is trained in a safe environment and exposed to attacks at inference time. The attacker aims at finding a perturbation of an instance that changes the model outcome.We propose a model-agnostic strategy that builds a robust ensemble by training its basic models on feature-based partitions of the given dataset. Our algorithm guarantees that the majority of the models in the ensemble cannot be affected by the attacker. We apply the proposed strategy to decision tree ensembles, and we also propose an approximate certification method for tree ensembles that efficiently provides a lower bound of the accuracy of a forest in the presence of attacks on a given dataset avoiding the costly computation of evasion attacks.Experimental evaluation on publicly available datasets shows that the proposed feature partitioning strategy provides a significant accuracy improvement with respect to competitor algorithms and that the proposed certification method allows ones to accurately estimate the effectiveness of a classifier where the brute-force approach would be unfeasible.

Using Model Checking in a Parallelizing Compiler

1998 ◽  
Vol 08 (04) ◽  
pp. 459-471 ◽  
Author(s):  
Teodor Rus ◽  
Eric van Wyk
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Data Dependence ◽  
Parallelizing Compiler ◽  
Model Checker ◽  
Source Program ◽  
Formal Framework ◽  
Sequential Processes ◽  
Logic Model Checking

In this paper we describe the usage of temporal logic model checking in a parallelizing compiler to analyze the structure of a source program and locate opportunities for optimization and parallelization. The source program is represented as a process graph in which the nodes are sequential processes and the edges are control and data dependence relationships between the computations at the nodes. By labeling the nodes and edges with descriptive atomic propositions and by specifying the conditions necessary for optimizations and parallelizations as temporal logic formulas, we can use a model checker to locate nodes of the process graph where particular optimizations can be made. To discover opportunities for new optimizations or modify existing ones in this parallelizing compiler, we need only specify their conditions as temporal logic formulas; we do not need to add to or modify the code of the compiler. This greatly simplifies the process of locating optimization and parallelization opportunities in the source program and makes it easier to experiment with complex optimizations. Hence, this methodology provides a convenient, concise, and formal framework in which to carry out program optimizations by compilers.

scholarly journals Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations

2021 ◽  
Vol 5 (4) ◽  
pp. 1-25
Author(s):  
Colin Shea-Blymyer ◽  
Houssam Abbas
Keyword(s):  
Model Checking ◽  
Deontic Logic ◽  
Autonomous Vehicle ◽  
Autonomous Systems ◽  
Automatic Reasoning ◽  
Starting Point ◽  
Formal Framework ◽  
Act Utilitarianism ◽  
Self Driving Cars

In this article, we develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions, and prohibitions are distinct from a system's mission, and are a necessary part of specifying advanced, adaptive AI-equipped systems. They need a dedicated deontic logic of obligations to formalize them. Most existing deontic logics lack corresponding algorithms and system models that permit automatic verification. We demonstrate how a particular deontic logic, Dominance Act Utilitarianism (DAU) [23], is a suitable starting point for formalizing the obligations of autonomous systems like self-driving cars. We demonstrate its usefulness by formalizing a subset of Responsibility-Sensitive Safety (RSS) in DAU; RSS is an industrial proposal for how self-driving cars should and should not behave in traffic. We show that certain logical consequences of RSS are undesirable, indicating a need to further refine the proposal. We also demonstrate how obligations can change over time, which is necessary for long-term autonomy. We then demonstrate a model-checking algorithm for DAU formulas on weighted transition systems and illustrate it by model-checking obligations of a self-driving car controller from the literature.

scholarly journals Local Model Checking and Traces

1994 ◽  
Vol 1 (17) ◽  
Author(s):  
Allan Cheng
Keyword(s):  
Model Checking ◽  
Polynomial Time ◽  
Transition System ◽  
Satisfiability Problem ◽  
Local Model ◽  
Transition Systems ◽  
Finite Systems ◽  
Soundness And Completeness ◽  
The Given ◽  
Local Model Checking

We present a <em>CTL</em>-like logic which is interpreted over labeled asynchronous transition systems. The interpretation reflects the desire to reason about these only with respect their progress fair behaviours. For finite systems we provide a set of tableau rules and prove soundness and completeness with respect to the given interpretation of our logic. We also provide a model checking algorithm which solves the model checking problem in deterministic polynomial time in the size of the formula and the labelled asynchronous transition system. We then consider different extensions of the logic with modalities expressing concurrent behaviour and investigate how this affects the decidability of the satisfiability problem.

scholarly journals Formalizing Group and Propagated Trust in Multi-Agent Systems

2020 ◽  
Author(s):  
Nagat Drawel ◽  
Jamal Bentahar ◽  
Amine Laarej ◽  
Gaith Rjoub
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Reduction Technique ◽  
Branching Time ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Formal Framework ◽  
Multi Agent

We present a formal framework that allows individual and group of agents to reason about their trust toward other agents. In particular, we propose a branching time temporal logic BT which includes operators that express concepts such as everyone trust, distributed trust and propagated trust. We analyze the satisfiability and model checking problems of this logic using a reduction technique.

Applying Formal Methods to Verify Web Services Orchestration and Choreography

2018 ◽  
pp. 221-243
Author(s):  
Zohra Sbai
Keyword(s):  
Model Checking ◽  
Web Services ◽  
Special Class ◽  
Added Value ◽  
Model Checker ◽  
Web Services Composition ◽  
Services Composition ◽  
Formal Framework ◽  
Services Orchestration ◽  
The Web

The contribution presented in this chapter is to provide a formal framework ensuring the model checking based verification of the Composition of Web Services (WSC). For this, the authors propose first to model the web services composition by an interaction of open workflow nets: a special class of Petri nets. Then, they detail how to check behavioral properties specified in temporal logic using the model checker NuSMV. A WSC is with added value only if the involved services are compatible. So, in this context, across the translation proposed, the authors develop a verification layer of the WSC compatibility. This work is developed in a framework named D&A4WSC which allows to model the WSC by oWF-nets and to check their compatibility by invoking the model checker NuSMV. Furthermore, the authors extended D&A4WSC so that it permits a web services choreography described in a WS-CDL specification. For this they developed a translation from WS-CDL to a composition of oWF-nets, so that one can verify this choreography by the aforementioned approach.

Sign in / Sign up

Export Citation Format

Share Document