![]() Menghi, Claudio ![]() 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: 122 (21 UL)![]() Menghi, Claudio ![]() in IEEE Transactions on Software Engineering (2019) Mobile and general-purpose robots increasingly support our everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing their complex behaviors ... [more ▼] Mobile and general-purpose robots increasingly support our everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing their complex behaviors known as missions. Recognizing this need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation or guiding implementation. For instance, the logical language LTL is commonly used by experts to specify missions as an input for planners, which synthesize the behavior a robot should have. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems, each of which detailing the usage intent, known uses, relationships to other patterns, and-most importantly-a template mission specification in temporal logic. Our tooling produces specifications expressed in the temporal logics LTL and CTL to be used by planners, simulators or model checkers. The patterns originate from 245 realistic textual mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios we defined with two well-known industrial partners developing human-size robots. We validated our patterns' correctness with simulators and two different types of real robots. [less ▲] Detailed reference viewed: 135 (20 UL)![]() ; Bianculli, Domenico ![]() 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: 352 (24 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE 2015) (2015, May) Detailed reference viewed: 174 (7 UL)![]() Bianculli, Domenico ![]() 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: 270 (34 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 7h International Conference on Service Oriented Computing and Application (SOCA 2014) (2014, November) Detailed reference viewed: 146 (3 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 6th International Symposium On Leveraging Applications of Formal Methods Verification and Validation (ISoLA 2014) (2014, October) Detailed reference viewed: 117 (1 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 12th International Conference on Software Engineering and Formal Methods (SEFM 2014) (2014, September) Detailed reference viewed: 180 (14 UL)![]() Bianculli, Domenico ![]() in Software Engineering 2014: Fachtagung des GI-Fachbereichs Softwaretechnik (2014, February) Detailed reference viewed: 82 (10 UL)![]() ; Bianculli, Domenico ![]() in Proceedings of the 6th International Workshop on Principles of Engineering Service-oriented Systems (PESOS 2014) (2014) Detailed reference viewed: 212 (2 UL)![]() ; Bianculli, Domenico ![]() in Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014) (2014) Detailed reference viewed: 269 (10 UL)![]() Bianculli, Domenico ![]() Report (2013) Detailed reference viewed: 95 (1 UL)![]() Bianculli, Domenico ![]() 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: 112 (5 UL)![]() Bianculli, Domenico ![]() 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: 185 (12 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 34th International Conference on Software Engineering (ICSE 2012) (2012) Detailed reference viewed: 124 (7 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 31st International Conference on Software Engineering (ICSE 2009), Vancouver, Canada (2009) Detailed reference viewed: 98 (0 UL)![]() Bianculli, Domenico ![]() in Proceedings of Principles of Engineering Service Oriented Systems (PESOS 2009), co-located with ICSE 2009, Vancouver, Canada (2009) Detailed reference viewed: 91 (1 UL)![]() Bianculli, Domenico ![]() 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: 98 (0 UL)![]() Bianculli, Domenico ![]() in Börger, Egon; Cisternino, Antonio (Eds.) Advances in Software Engineering (2008) Detailed reference viewed: 101 (0 UL)![]() Bianculli, Domenico ![]() in Proceedings of the 2nd International Workshop on Systems Development in SOA Environments (SDSOA 2008), co-located with ICSE 2008 (2008) Detailed reference viewed: 108 (2 UL) |
||