Lorenzo Capra

Lorenzo Capra

Petri Nets (PN) are a central, theoretically sound model for concurrent or distributed systems but, at least in their classical definition, not expressive enough to represent dynamic reconfiguration capabilities. On the other side, Rewriting Logic has proved to be a natural semantic framework for several formal models of concurrent/distributed systems. We propose a compact, efficient Maude formalization of dynamically reconfigurable PT nets (with inhibitor arcs), using as a running example the specification of a simple, fault-tolerant manufacturing system. We discuss the advantages of such a combined approach, as well as some concerns that it raises.

Carlo Bellettini, Matteo Camilli, Lorenzo Capra et al.

The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. In this paper we introduce a distributed approach which exploits techniques typically used by the "big data" community to enable verification of Computation Tree Logic (CTL) formulas on very large state spaces using distributed systems and cloud computing facilities. The outcome of several tests performed on benchmark specifications are presented, thus showing the convenience of the proposed approach.

Carlo Bellettini, Matteo Camilli, Lorenzo Capra et al.

The growing availability of distributed and cloud computing frameworks make it possible to face complex computational problems in a more effective and convenient way. A notable example is state-space exploration of discrete-event systems specified in a formal way. The exponential complexity of this task is a major limitation to the usage of consolidated analysis techniques and tools. We present and compare two different approaches to state-space explosion, relying on distributed and cloud frameworks, respectively. These approaches were designed and implemented following the same computational schema, a sort of map & fold. They are applied on symbolic state-space exploration of real-time systems specified by (a timed extension of) Petri Nets, by readapting a sequential algorithm implemented as a command-line Java tool. The outcome of several tests performed on a benchmarking specification are presented, thus showing the convenience of cloud approaches.