References of "Ghezzi, Carlo"
     in
Bookmark and Share    
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: 232 (22 UL)
Full Text
Peer Reviewed
See detailSyntax-driven program verification of matching logic properties.
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Proceedings of the 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE 2015) (2015, May)

Detailed reference viewed: 92 (7 UL)
Full Text
Peer Reviewed
See detailSyntactic-Semantic Incrementality for Agile Verification
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Science of Computer Programming (2015), 97(0), 47-54

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we ... [more ▼]

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we envision the seamless integration of automated verification techniques within agile methodologies, thanks to the support for incrementality. Incremental verification accommodates the changes that occur within the schedule of frequent releases of software agile processes. We propose a general approach to developing families of verifiers that can support incremental verification for different kinds of artifacts and properties. The proposed syntactic-semantic approach is rooted in operator precedence grammars and their support for incremental parsing. Incremental verification procedures are encoded as attribute grammars, whose incremental evaluation goes hand in hand with incremental parsing. [less ▲]

Detailed reference viewed: 191 (34 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: 65 (3 UL)
Full Text
Peer Reviewed
See detailIncremental Syntactic-Semantic Reliability Analysis of Evolving Structured Workflows
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Proceedings of the 6th International Symposium On Leveraging Applications of Formal Methods Verification and Validation (ISoLA 2014) (2014, October)

Detailed reference viewed: 52 (1 UL)
Full Text
Peer Reviewed
See detailTrace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce
Bianculli, Domenico UL; Ghezzi, Carlo; Krstić, Srđan

in Proceedings of the 12th International Conference on Software Engineering and Formal Methods (SEFM 2014) (2014, September)

Detailed reference viewed: 100 (10 UL)
Full Text
See detailSpecification Patterns from Research to Industry: A Case Study in Service-Based Applications (extended abstract)
Bianculli, Domenico UL; Ghezzi, Carlo; Pautasso, Cesare et al

in Software Engineering 2014: Fachtagung des GI-Fachbereichs Softwaretechnik (2014, February)

Detailed reference viewed: 44 (10 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: 143 (10 UL)
Full Text
Peer Reviewed
See detailTowards the formalization of properties of cloud-based elastic systems
Bersani, Marcello Maria; Bianculli, Domenico UL; Dustdar, Schahram et al

in Proceedings of the 6th International Workshop on Principles of Engineering Service-oriented Systems (PESOS 2014) (2014)

Detailed reference viewed: 128 (2 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: 49 (1 UL)
Full Text
See detailA Syntactic-Semantic Approach to Incremental Verification
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

E-print/Working paper (2013)

Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices ... [more ▼]

Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial. This paper introduces SiDECAR, a general framework for the definition of verification procedures, which are made incremental by the framework itself. Verification procedures are driven by the syntactic structure (defined by a grammar) of the system and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. We show the application of SiDECAR to the definition of two verification procedures: probabilistic verification of reliability requirements and verification of safety properties. [less ▲]

Detailed reference viewed: 69 (5 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: 100 (12 UL)
Full Text
Peer Reviewed
See detailSpecification Patterns from Research to Industry: a Case Study in Service-based Applications
Bianculli, Domenico UL; Ghezzi, Carlo; Pautasso, Cesare et al

in Proceedings of the 34th International Conference on Software Engineering (ICSE 2012) (2012)

Detailed reference viewed: 63 (4 UL)
Full Text
Peer Reviewed
See detailReMan: A Pro-active Reputation Management Infrastructure for Composite Web Services
Bianculli, Domenico UL; Binder, Walter; Drago, Luigi et al

in Proceedings of the 31st International Conference on Software Engineering (ICSE 2009), Vancouver, Canada (2009)

Detailed reference viewed: 37 (0 UL)
Full Text
Peer Reviewed
See detailEmbedding Continuous Lifelong Verification in Service Life Cycles
Bianculli, Domenico UL; Ghezzi, Carlo; Pautasso, Cesare

in Proceedings of Principles of Engineering Service Oriented Systems (PESOS 2009), co-located with ICSE 2009, Vancouver, Canada (2009)

Detailed reference viewed: 35 (1 UL)
Full Text
Peer Reviewed
See detailA Guided Tour through SAVVY-WS: a Methodology for Specifying and Validating Web Service Compositions
Bianculli, Domenico UL; Ghezzi, Carlo; Spoletini, Paola et al

in Börger, Egon; Cisternino, Antonio (Eds.) Advances in Software Engineering (2008)

Detailed reference viewed: 40 (0 UL)
Full Text
Peer Reviewed
See detailTransparent Reputation Management for Composite Web Services
Bianculli, Domenico UL; Binder, Walter; Drago, Luigi et al

in Proceedings of the IEEE International Conference on Web Services (ICWS 2008), Beijing, China (2008)

Detailed reference viewed: 41 (0 UL)
Full Text
Peer Reviewed
See detailTowards a methodology for lifelong validation of service compositions
Bianculli, Domenico UL; Ghezzi, Carlo

in Proceedings of the 2nd International Workshop on Systems Development in SOA Environments (SDSOA 2008), co-located with ICSE 2008 (2008)

Detailed reference viewed: 48 (2 UL)
Full Text
Peer Reviewed
See detailSAVVY-WS at a glance: supporting verifiable dynamic service compositions
Bianculli, Domenico UL; Ghezzi, Carlo

in Proceedings of the 1st International Workshop on Automated engineeRing of Autonomous and run-tiMe evolvIng Systems (ARAMIS 2008), co-located with ASE 2008 (2008)

Detailed reference viewed: 37 (0 UL)
Full Text
Peer Reviewed
See detailMonitoring Conversational Web Services
Bianculli, Domenico UL; Ghezzi, Carlo

in Proceedings of the 2nd International Workshop on Service-Oriented Software Engineering (IW-SOSWE'07) co-located with ESEC/FSE 2007 (2007)

Detailed reference viewed: 39 (0 UL)