References of "Spoletini, Paola"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailA verification-driven framework for iterative design of controllers
Menghi, Claudio UL; Spoletini, Paola; Chechik, Marsha et al

in Formal Aspects of Computing (2019), 31

Controllers often are large and complex reactive software systems and thus they typically cannot be developed as monolithic products. Instead, they are usually comprised of multiple components that ... [more ▼]

Controllers often are large and complex reactive software systems and thus they typically cannot be developed as monolithic products. Instead, they are usually comprised of multiple components that interact to provide the desired functionality. Components themselves can be complex and in turn be decomposed into multiple sub-components. Designing such systems is complicated and must follow systematic approaches, based on recursive decomposition strategies that yield a modular structure. This paper proposes FIDDle–a comprehensive verification-driven framework which provides support for designers during development. FIDDle supports hierarchical decomposition of components into sub-components through formal specification in terms of pre- and post-conditions as well as independent development, reuse and verification of sub-components. The framework allows the development of an initial, partially specified design of the controller, in which certain components, yet to be defined, are precisely identified. These components can be associated with pre- and post-conditions, i.e., a contract, that can be distributed to third-party developers. The framework ensures that if the components are compliant with their contracts, they can be safely integrated into the initial partial design without additional rework. As a result, FIDDle supports an iterative design process and guarantees correctness of the system at any step of development. We evaluated the effectiveness of FIDDle in supporting an iterative and incremental development of components using the K9 Mars Rover example developed at NASA Ames. This can be considered as an initial, yet substantive, validation of the approach in a realistic setting. We also assessed the scalability of FIDDle by comparing its efficiency with the classical model checkers implemented within the LTSA toolset. Results show that FIDDle scales as well as classical model checking as the number of the states of the components under development and their environments grow. [less ▲]

Detailed reference viewed: 62 (19 UL)
Full Text
See detailKeep It Small, Keep It Real: Efficient Run-time Verification of Web Service Compositions
Baresi, Luciano; Bianculli, Domenico UL; Guinea, Sam et al

Report (2009)

Detailed reference viewed: 74 (2 UL)
Full Text
Peer Reviewed
See detailKeep It Small, Keep It Real: Efficient Run-time Verification of Web Service Compositions
Baresi, Luciano; Bianculli, Domenico UL; Guinea, Sam et al

in Proceedings of IFIP international conference on Formal Techniques for Distributed Systems (FMOODS/FORTE 2009) (2009)

Detailed reference viewed: 71 (2 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: 64 (0 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: 25 (0 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: 82 (2 UL)
Full Text
Peer Reviewed
See detailValidation of web service compositions
Baresi, Luciano; Bianculli, Domenico UL; Ghezzi, Carlo et al

in IET Software (2007), 1(6), 219--232

Detailed reference viewed: 70 (0 UL)
Full Text
Peer Reviewed
See detailA model checking approach to verify BPEL4WS workflows
Bianculli, Domenico UL; Ghezzi, Carlo; Spoletini, Paola

in Proceedings of the 2007 IEEE International Conference on Service-Oriented Computing and Applications (IEEE SOCA 2007) (2007)

Detailed reference viewed: 70 (1 UL)
Full Text
Peer Reviewed
See detailA Timed extension of WSCoL
Baresi, Luciano; Bianculli, Domenico UL; Ghezzi, Carlo et al

in Proceedings of the IEEE International Conference on Web Services (ICWS 2007) (2007)

Detailed reference viewed: 58 (0 UL)