This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through ...the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics. We extend these study and applied the above methodology on parallel approaches, especially to refine the sharing measure which shows promising results.
Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SATisfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It ...consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration-Exploitation using Exponential weight (EXP3), that allows smart resource allocations. Our contribution is adapted to situations where we have to solve a bench of SAT instances issued from one or several sequence of problems. Our experiments show that our approach achieves good results.
The BPMN standard notation allows business process designers to model both intra-organizational processes and inter-organizational collaborations. A great effort has been devoted in proposing formal ...semantics for BPMN, and, fewer, in providing dedicated verification tools. Still, some advanced features of BPMN, namely communication or time-related constructs, are often set aside. This becomes an issue as BPMN gains interest outside of its original scope, e.g., for the IoT where communication and time play an important role. In this paper, we propose a formal semantics for a subset of BPMN. This semantics takes into account not only the usual gateways, but also sub-processes, inter-process communication, and time-related constructs. In contrast to transformational approaches, which give a semantics to BPMN by mapping it to some formal model (e.g., transition systems or Petri nets), our approach is based on a direct formalization in first-order logic that is then realized in a straightforward way into the TLA+ formal language. We build on the TLA+ model-checker, TLC, to provide process designers with a verification framework, fbpmn, that one may use to check BPMN and workflow specific properties. Our tools and our model database are open source and freely available online.
•A direct formal semantics for a subset of BPMN, including sub-processes, communication and time constructs.•Automated verification of intra-organization workflows and inter-organization collaborations.•Seven models for communication, two models for time.•Communication models and properties of interest are easily extensible.•Open source and freely available tools and model repository.
Tuning SAT solvers for LTL Model Checking Kheireddine, Anissa; Renault, Etienne; Baarir, Souheib
2022 29th Asia-Pacific Software Engineering Conference (APSEC),
2022-Dec.
Conference Proceeding
Odprti dostop
Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, which are supposed to work for any SAT ...problem. The key idea defended in this paper is to tune SAT solvers algorithm using: (1) a static classification based on the variables used to encode the BMC into a Boolean formula; (2) and use the hierarchy of Manna&Pnueli 33 that classmes any property expressed through Linear-time Temporal Logic (LTL). By combining these two information with the classical Literal Block Distance (LBD) measure 46, we designed a new heuristic, well suited for solving BMC problems. In particular, our work identifies and exploits a new set of relevant (learnt) clauses. We experiment with these ideas by developing a tool dedicated for SAT-based LTL BMC solvers, called BSaLTic. Our experiments over a large database of BMC problems, show promising results. In particular, BSaLTic provides good performance on UNSAT problems. This work highlights the importance of considering the structure of the underlying problem in SAT procedures.
Nowadays, a wide range of systems are becoming structurally dynamic, variably interconnected, and highly complex. The use of classical formal approaches, such as Petri nets, in the design of such ...systems becomes neither convenient nor sufficient. Indeed, they cannot handle, in a natural way, the dynamic structure and the growing complexity of modern systems.
Introducing reconfigurability in Petri nets, as well as generalized stochastic Petri nets increases the modeling power, but decreases the applicability of analysis techniques. In fact, several properties become undecidable
In this paper, we extend generalized stochastic Petri nets to a reconfigurable formalism, while maintaining verifiability with reduced complexity. The proposed approach identifies a set of properties that are preserved after reconfiguration. These properties are decidable with reduced time and space complexity. The use of the proposed formalism is illustrated through a running example.
•A new Petri nets based formalism is proposed for reconfigurable systems.•The new formalism handles two aspects: stochastic time and reconfigurability.•Improved Net Rewriting Systems and Generalized Stochastic Petri Nets are combined.•A new approach for the performance evaluation is proposed and exploited.•The formalism is exploited in an Reconfigurable Manufacturing Systems case study.
PDF
