Search

Model design is not a linear, one-shot process. It proceeds through refinements and revisions. To effectively support developers in generating model refinements and revisions, it is desirable to have some automated support to verify evolvable models. To address this problem, we recently proposed to adopt topological proofs, which are slices of the original model that witness property satisfaction. We implemented TOrPEDO, a framework that provides automated support for using topological proofs during model design. Our results showed that topological proofs are significantly smaller than the original models, and that, in most of the cases, they allow the property to be re-verified by relying only on a simple syntactic check. However, our results also show that the procedure that computes topological proofs, which requires extracting unsatisfiable cores of LTL formulae, is computationally expensive. For this reason, TOrPEDO currently handles models with a small dimension. With the intent of providing practical and efficient support for flexible model design and wider adoption of our framework, in this paper, we propose an enhanced—re-engineered—version of TOrPEDO. The new version of TOrPEDO relies on a novelprocedure to extract topological proofs, which has so far represented the bottleneck of TOrPEDO performances. We implemented our procedure within TOrPEDO by considering Partial Kripke Structures (PKSs) and Linear-time Temporal Logic (LTL): two widely used formalisms to express models with uncertain parts and their properties. To extract topological proofs, the new version of TOrPEDO converts the LTL formulae into an SMT instance and reuses an existing SMT solver (e.g., Microsoft Z3) to compute an unsatisfiable core. Then, the unsatisfiable core returned by the SMT solver is automatically processed to generate the topological proof. We evaluated TOrPEDO by assessing (i) how does the size of the proofs generated by TOrPEDO compares to the size of the models being analyzed; and (ii) how frequently the use of the topological proof returned by TOrPEDO avoids re-executing the model checker. Our results show that TOrPEDO provides proofs that are smaller (≈60%) than their respective initial models effectively supporting designers in creating model revisions. In a significant number of cases (≈79%), the topological proofs returned by TOrPEDO enable assessing the property satisfaction without re-running the model checker. We evaluated our new version of TOrPEDO by assessing (i) how it compares to the previous one; and (ii) how useful it is in supporting the evaluation of alternative design choices of (small) model instances in applied domains. The results show that the new version of TOrPEDO is significantly more efficient than the previous one and can compute topological proofs for models with less than 40 states within two hours. The topological proofs and counterexamples provided by TOrPEDO are useful to support the development of alternative design choices of (small) model instances in applied domains.

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.

As researchers and teachers and practitioners, we “software types” excel at multitasking. This, in part, led us to ask the question: Can one attend a software engineering conference and do something good for society? We found the answer to be a resounding yes. In this article, we present our first experience of running RE Cares, a conference collocated event. This event included a workshop, conference sessions, and a hackathon for developing an application to support emergency field activity for Mutual Aid Alberta, a nonprofit organization coordinating natural disaster responses in the Canadian province.

Modern Building Management Systems (BMSs) have been designed to automate the behavior of complex buildings, but unfortunately they do not allow occupants to customize it according to their preferences, and only the facility manager is in charge of setting the building policies. To overcome this limitation, we present BuildingRules, a trigger-action programming-based system that aims to provide occupants of commercial buildings with the possibility of specifying the characteristics of their office environment through an intuitive interface. Trigger-action programming is intuitive to use and has been shown to be effective in meeting user requirements in home environments. To extend this intuitive interface to commercial buildings, an essential step is to manage the system scalability as large number of users will express their policies. BuildingRules has been designed to scale well for large commercial buildings as it automatically detects conflicts that occur among user specified policies and it supports intelligent grouping of rules to simplify the policies across large numbers of rooms. We ensure the conflict resolution is fast for a fluid user experience by using the Z3 SMT solver. BuildingRules backend is based on RESTful web services so it can connect to various BMSs and scale well with large number of buildings. We have tested our system with 23 users across 17 days in a virtual office building, and the results we have collected prove the effectiveness and the scalability of BuildingRules.

XML is becoming widespread as data interoperability standard in many application domains. An increasing number of researchers and professionals, who are not computer scientists (although they may have a strong technical background), needs to query and transform XML data during their working activities. Such tasks typically require simple queries and partial awareness of the XML data model, in the context of a given, domain-specific XML-based protocol. The W3C community has proposed XQuery as the standard query language for XML [9]. XQuery has a huge expressive power - as it encompasses features belonging both to query and functional languages, but it may be considered as too complex for the above user profiles; well-designed subsets of XQuery are sufficient to satisfy their needs. In this paper, we propose six layered subsets of XQuery, targeted to cover user communities with increasing needs. The initial layers are based upon XQBE (XQuery By Example), a visual XML query language, strictly less expressive than XQuery. We argue that the first layers are easier to learn and to master than the full language, also thanks to the availability of simple visual interfaces, and that these layers cover most of the needs of many user communities.