scholarly journals TOrPEDO: witnessing model correctness with topological proofs

2021 ◽  
Author(s):  
Claudio Menghi ◽  
Alessandro Maria Rizzi ◽  
Anna Bernasconi ◽  
Paola Spoletini
Keyword(s):  
Linear Time ◽  
Small Dimension ◽  
Model Design ◽  
Model Checker ◽  
Smt Solver ◽  
Alternative Design ◽  
Topological Proof ◽  
Small Model ◽  
Automated Support ◽  
Unsatisfiable Core

AbstractModel design is not a linear, one-shot process. It proceeds through refinements and revisions. To effectively support developers in generating model refinements and revisions, it is desirable to have some automated support to verify evolvable models. To address this problem, we recently proposed to adopt topological proofs, which are slices of the original model that witness property satisfaction. We implemented , a framework that provides automated support for using topological proofs during model design. Our results showed that topological proofs are significantly smaller than the original models, and that, in most of the cases, they allow the property to be re-verified by relying only on a simple syntactic check. However, our results also show that the procedure that computes topological proofs, which requires extracting unsatisfiable cores of LTL formulae, is computationally expensive. For this reason, currently handles models with a small dimension. With the intent of providing practical and efficient support for flexible model design and wider adoption of our framework, in this paper, we propose an enhanced—re-engineered—version of . The new version of relies on a novel procedure to extract topological proofs, which has so far represented the bottleneck of performances. We implemented our procedure within by considering Partial Kripke Structures (PKSs) and Linear-time Temporal Logic (LTL): two widely used formalisms to express models with uncertain parts and their properties. To extract topological proofs, the new version of converts the LTL formulae into an SMT instance and reuses an existing SMT solver (e.g., Microsoft ) to compute an unsatisfiable core. Then, the unsatisfiable core returned by the SMT solver is automatically processed to generate the topological proof. We evaluated by assessing (i) how does the size of the proofs generated by compares to the size of the models being analyzed; and (ii) how frequently the use of the topological proof returned by avoids re-executing the model checker. Our results show that provides proofs that are smaller ($$\approx $$ ≈ 60%) than their respective initial models effectively supporting designers in creating model revisions. In a significant number of cases ($$\approx $$ ≈ 79%), the topological proofs returned by enable assessing the property satisfaction without re-running the model checker. We evaluated our new version of by assessing (i) how it compares to the previous one; and (ii) how useful it is in supporting the evaluation of alternative design choices of (small) model instances in applied domains. The results show that the new version of is significantly more efficient than the previous one and can compute topological proofs for models with less than 40 states within two hours. The topological proofs and counterexamples provided by are useful to support the development of alternative design choices of (small) model instances in applied domains.

Enhancing the application potential of dissipative controlled rocking connections through detailing and design

2021 ◽  
Author(s):  
Brandon McHaffie ◽  
Peter Routledge ◽  
Alessandro Palermo
Keyword(s):  
Linear Time ◽  
Time History ◽  
Cost Effective ◽  
Real Structure ◽  
Construction Costs ◽  
Alternative Design ◽  
Design Philosophy ◽  
History Analysis ◽  
Application Potential ◽  
The University

<p>Research on low-damage systems has been significant in the past decade. These systems combine post- tensioning, which provides self-centring; and typically use replaceable devices, which give energy dissipation. WSP has used recent research, carried out at the University of Canterbury, on low-damage bridge piers and applied this into a real structure – the Wigram-Magdala Link Bridge. This is believed to be the first bridge in New Zealand and possibly worldwide to adopt such a system. Given this was the first application of the system to a real structure, there were some valuable learnings during design and construction. Firstly, the application of axial dissipaters has some limitations due to available material sizes, construction difficulty and aesthetics. Secondly, there is still some additional cost and complexity associated with using the low-damage system. Given these difficulties, this paper presents an alternative design philosophy which better captures the benefits of the low-damage system, which include cost-effective repair method, controlled damage and additional robustness and resilience. The alternative design philosophy presented is expected to result in reduced construction costs by reducing pier and foundation demands. Peak displacements and forces will be compared to the results from non-linear time history analysis to verify the performance of the low-damage connection using scaled ground motions. Furthermore, the paper will present the possible application of an alternative dissipation device, the lead extrusion damper, which can further improve the performance of low-damage connections.</p>

scholarly journals Using a bounded model checker for test generation: How to kill two birds with one SMT solver

2015 ◽  
Vol 49 (7) ◽  
pp. 466-472 ◽  
Author(s):  
M. Petrov ◽  
K. Gagarski ◽  
M. Belyaev ◽  
V. Itsykson
Keyword(s):  
Test Generation ◽  
Model Checker ◽  
Smt Solver

scholarly journals Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems

2018 ◽  
Author(s):  
Chen Fu ◽  
Andrea Turrini ◽  
Xiaowei Huang ◽  
Lei Song ◽  
Yuan Feng ◽  
...  
Keyword(s):  
Linear Programming ◽  
Model Checking ◽  
Multiagent Systems ◽  
Epistemic Logic ◽  
Mixed Integer ◽  
Model Checker ◽  
Non Linear Programming ◽  
Smt Solver ◽  
Realistic Assumption ◽  
Novel Algorithm

In this work we study the model checking problem for probabilistic multiagent systems with respect to the probabilistic epistemic logic PETL, which can specify both temporal and epistemic properties. We show that under the realistic assumption of uniform schedulers, i.e., the choice of every agent depends only on its observation history, PETL model checking is undecidable. By restricting the class of schedulers to be memoryless schedulers, we show that the problem becomes decidable. More importantly, we design a novel algorithm which reduces the model checking problem into a mixed integer non-linear programming problem, which can then be solved by using an SMT solver. The algorithm has been implemented in an existing model checker and experiments are conducted on examples from the IPPC competitions.

scholarly journals Interpolation and Model Checking for Nonlinear Arithmetic

2021 ◽  
pp. 266-288
Author(s):  
Dejan Jovanović ◽  
Bruno Dutertre
Keyword(s):  
Model Checking ◽  
Satisfiability Modulo Theories ◽  
Full Model ◽  
Model Checker ◽  
New Model ◽  
Smt Solver ◽  
Partial Model ◽  
Interpolation Procedure ◽  
State Of Art ◽  
Nonlinear Arithmetic

AbstractWe present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic.

scholarly journals Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories

2011 ◽  
Vol 40 ◽  
pp. 701-728 ◽  
Author(s):  
A. Cimatti ◽  
A. Griggio ◽  
R. Sebastiani
Keyword(s):  
Empirical Test ◽  
Main Idea ◽  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
The Core ◽  
Reduction Techniques ◽  
Novel Approach ◽  
Suitable Amount ◽  
Core Reduction ◽  
Unsatisfiable Core

The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT. Surprisingly, the problem of finding unsatisfiable cores in SMT has received very little attention in the literature. In this paper we present a novel approach to this problem, called the Lemma-Lifting approach. The main idea is to combine an SMT solver with an external propositional core extractor. The SMT solver produces the theory lemmas found during the search, dynamically lifting the suitable amount of theory information to the Boolean level. The core extractor is then called on the Boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas are removed. The approach is conceptually interesting, and has several advantages in practice. In fact, it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play manner, so as to benefit for free of all unsat-core reduction techniques which have been or will be made available. We have evaluated our algorithm with a very extensive empirical test on SMT-LIB benchmarks, which confirms the validity and potential of this approach.

scholarly journals Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT-solver

2014 ◽  
Vol 21 (6) ◽  
pp. 83-93
Author(s):  
Maxim Petrov ◽  
Kirill Gagarski ◽  
Mikhail Belyaev ◽  
Vladimir Itsykson
Keyword(s):  
Test Generation ◽  
Model Checker ◽  
Smt Solver

A Real Time Control Architecture for Continuously Managing Patients in a Care Unit

1995 ◽  
Vol 34 (05) ◽  
pp. 475-488
Author(s):  
B. Seroussi ◽  
J. F. Boisvieux ◽  
V. Morice
Keyword(s):  
Real Time ◽  
Linear Time ◽  
Treatment Plan ◽  
Control Architecture ◽  
Real Time Control ◽  
Time Representation ◽  
Time Control ◽  
Continuous Support ◽  
Definition Of ◽  
Computerized System

Abstract:The monitoring and treatment of patients in a care unit is a complex task in which even the most experienced clinicians can make errors. A hemato-oncology department in which patients undergo chemotherapy asked for a computerized system able to provide intelligent and continuous support in this task. One issue in building such a system is the definition of a control architecture able to manage, in real time, a treatment plan containing prescriptions and protocols in which temporal constraints are expressed in various ways, that is, which supervises the treatment, including controlling the timely execution of prescriptions and suggesting modifications to the plan according to the patient’s evolving condition. The system to solve these issues, called SEPIA, has to manage the dynamic, processes involved in patient care. Its role is to generate, in real time, commands for the patient’s care (execution of tests, administration of drugs) from a plan, and to monitor the patient’s state so that it may propose actions updating the plan. The necessity of an explicit time representation is shown. We propose using a linear time structure towards the past, with precise and absolute dates, open towards the future, and with imprecise and relative dates. Temporal relative scales are introduced to facilitate knowledge representation and access.

Sign in / Sign up

Export Citation Format

Share Document