References of "San Pietro, Pierluigi"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailModel Checking MITL formulae on Timed Automata: a Logic-Based Approach
Menghi, Claudio UL; Bersani, Marcello; Rossi, Matteo et al

in ACM Transactions on Computational Logic (2020), 21(3),

Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for ... [more ▼]

Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts. This paper presents a novel technique to perform model checking of Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula which is verified through an available decision procedure. The technique is flexible since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures. [less ▲]

Detailed reference viewed: 151 (17 UL)
Full Text
Peer Reviewed
See detailEfficient Large-scale Trace Checking Using MapReduce
Bersani, Marcello Maria; Bianculli, Domenico UL; Ghezzi, Carlo et al

in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016) (2016, May)

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic ... [more ▼]

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs. [less ▲]

Detailed reference viewed: 341 (24 UL)
Full Text
Peer Reviewed
See detailOffline Trace Checking of Quantitative Properties of Service-Based Applications
Bianculli, Domenico UL; Ghezzi, Carlo; Krstić, Srđan et al

in Proceedings of the 7h International Conference on Service Oriented Computing and Application (SOCA 2014) (2014, November)

Detailed reference viewed: 135 (3 UL)
Full Text
Peer Reviewed
See detailSMT-based Checking of SOLOIST over Sparse Traces
Bersani, Marcello Maria; Bianculli, Domenico UL; Ghezzi, Carlo et al

in Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014) (2014)

Detailed reference viewed: 256 (10 UL)
See detailFrom SOLOIST to CLTLB(D): Checking quantitative properties of service-based applications
Bianculli, Domenico UL; Krstic, Srđan; Ghezzi, Carlo et al

Report (2013)

Detailed reference viewed: 83 (1 UL)
Full Text
Peer Reviewed
See detailThe tale of SOLOIST: a specification language for service compositions interactions
Bianculli, Domenico UL; Ghezzi, Carlo; San Pietro, Pierluigi

in Păsăreanu, Corina; Salaün, Gwen (Eds.) Formal Aspects of Component Software (2012, September)

Service-based applications are a new class of software systems that provide the basis for enterprises to build their information systems by following the principles of service-oriented architectures ... [more ▼]

Service-based applications are a new class of software systems that provide the basis for enterprises to build their information systems by following the principles of service-oriented architectures. These software systems are often realized by orchestrating remote, third-party services, to provide added-values applications that are called service compositions. The distributed ownership and the evolving nature of the services involved in a service composition make verification activities crucial. On a par with verification is also the problem of formally specifying the interactions—with third-party services—of service compositions, with the related issue of balancing expressiveness and support for automated verification. This paper showcases SOLOIST, a specification language for formalizing the interactions of service compositions. SOLOIST has been designed with the primary objective of expressing the most significant specification patterns found in the specifications of service-based applications. The language is based on a many-sorted first-order metric temporal logic, extended with new temporal modalities that support aggregate operators for events occurring in a certain time window. We also show how, under certain assumptions, the language can be reduced to linear temporal logic, paving the way for using SOLOIST with established verification techniques, both at design time and at run time. [less ▲]

Detailed reference viewed: 173 (12 UL)
Full Text
Peer Reviewed
See detailTrio2Promela: a Model Checker for Temporal Metric Specifications
Bianculli, Domenico UL; Morzenti, Angelo; Pradella, Matteo et al

in ICSE 2007 Companion: Companion of the proceedings of the 29th International Conference on Software Engineering (2007)

Detailed reference viewed: 117 (2 UL)
Full Text
Peer Reviewed
See detailModel checking temporal metric specification with Trio2Promela
Bianculli, Domenico UL; Spoletini, Paola; Morzenti, Angelo et al

in Proceedings of International Symposium on Fundamentals of Software Engineering (FSEN 2007) Teheran, Iran (2007)

Detailed reference viewed: 42 (0 UL)