Previous applications of symbolic execution (Sym-Exe) have focused on bug-finding and test-case generation. However, SymExe has the potential to significantly improve usability and automation when applied to verification of software contracts in safety-critical systems. Due to the lack of support for processing software contracts and ad hoc approaches for introducing a variety of over/under-approximations and optimizations, most SymExe implementations cannot precisely characterize the verification status of contracts. Moreover, these tools do not provide explicit justifications for their conclusions, and thus they are not aligned with trends toward evidence-based verification and certification. We introduce the concept of explicating symbolic execution (xSymExe) that builds on a strong semantic foundation, supports full verification of rich software contracts, explicitly tracks where over/under-approximations are introduced or avoided, precisely characterizes the verification status of each contractual claim, and associates each claim with explications for its reported verification status. We report on case studies in the use of Bakar Kiasan, our open source xSymExe tool for Spark Ada.

User Interface (UI) development methods are poorly integrated with standard software engineering practice. The differences in terms of artifacts involved, development philosophies, and lifecycles can often result in inconsistent system and UI specifications leading to duplication of effort and increased maintenance costs. To address such shortcomings, we propose an integrated development methodology for use case and task models. Use cases are generally used to capture functional requirements whereas task models specify the detailed user interactions with the UI. Our methodology can assist practitioners in developing software processes which allow these two kinds of artifacts to be developed in a codependent and integrated manner. We present our methodology, describe its semantic foundations along with a set of formal conformance relations, and introduce an automated verification tool.

Abstract Use case models are the specification medium of choice for functional requirements, while task models are employed to capture User Interface (UI) requirements and design information. In current practice, both entities are treated independently and are often developed by different teams, which have their own philosophies and lifecycles. This lack of integration is problematic and often results in inconsistent functional and UI design specifications causing duplication of effort while increasing the maintenance overhead. To address these shortcomings, we propose a formal semantic framework for the integrated development of use case and task models. The semantic mapping is defined in a two step manner from a particular use case or task model notation to the common semantic domain of sets of partially ordered sets . This two-step mapping results in a semantic framework that can be more easily reused and extended. The intermediate semantic domains have been carefully chosen by taking into consideration the intrinsic characteristics of use case and task models. As a concrete example, we provide a semantics for our own DSRG use case formalism and an extended version of ConcurTaskTrees, one of the most popular task model notations. Furthermore, we use the common semantic model to formally define a set of refinement relations for use case and task models.

Black box testing focuses on the core functionality of the system, while user interface testing is concerned with details of user interactions. Functional and user interface test cases are usually generated from two distinct system models, one for the functionality and one for the user interface. As a result, test cases derived from either model capture only partial system behavior and as such, are inadequate for testing full system behavior. We propose a method for formally integrating the model for the system functionality and the model for the user interface. The resulting composite model is then used to generate more complete test cases, capturing detailed user interactions as well as secondary system interactions. In this paper we employ use cases for modeling system functionality, and task models for describing user interfaces.

The Verifying Compiler (VC) project is a core component of the Dependable Systems Evolution Grand Challenge. The VC offers the promise of automatically proving that a program or component is correct, where correctness is defined by program assertions. While several VC prototypes exist, all adopt a semantics for assertions that is unsound. This paper presents a consolidation of VC requirements analysis (RA) activities that, in particular, brought us to ask targeted VC customers what kind of semantics they wanted. Taking into account both practitioners' needs and current technological factors, we offer recovery of soundness through an adjusted definition of assertion validity that matches user expectations and can be implemented practically using current prover technology. For decades, there have been debates concerning the most appropriate semantics for program assertions. Our contribution here is unique in that we have applied fundamental software engineering techniques by asking primary stakeholders what they want and, based on this, proposed a means of efficiently realizing the semantics stakeholders want using standard tools and techniques. We describe how support for the new semantics has been added to ESC/Java2, one of the most fully developed VC prototypes. Case studies demonstrate the effectiveness of the new semantics at uncovering previously indiscernible specification errors.

As a Behavioral Interface Specification Language (BISL) for Java, the Java Modeling Language (JML) is tightly coupled to the base language it enhances. Up until Java 1.4, JML kept apace with the evolution of its base language. Java 5 and subsequent revisions have yet to be fully supported by JML tools. Recent efforts such as JML4 have been addressing this issue by providing an Eclipse-based tooling infrastructure. In its current form, JML4 has a fairly steep learning curve for developers wishing to contribute to or extend it. To address this issue and bring JML tools one step closer to a desired plug-in model, we propose a JML Intermediate Representation (JIR) and supporting software infrastructure for JML front-ends and back-ends.

Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the `right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXPSPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

Use case models are the artifact of choice for capturing functional requirements. This typically collaborative activity makes merging a necessity. Use cases however, are often neglected when it comes to model merging, since they are commonly treated as text only items. By defining a formal syntax and semantics for use case models, manipulated within a generic metamodel for operation-based merging, we show how use case models can be effectively merged. This formal foundation allows for the modeling of use cases; defining meaningful change operations on them; and for detecting modeling inconsistencies, inconformities, and conflicts. Several practical examples validate the concepts presented: existing and planned tool support is introduced.

The verifying compiler (VC) project is a core component of the dependable systems evolution grand challenge. The VC offers the promise of automatically proving that a program or component is correct, where correctness is defined by program assertions. While several VC prototypes exist, all adopt a semantics for assertions that is unsound. This paper presents a consolidation of VC requirements analysis activities that, in particular, brought us to ask targeted VC customers what kind of semantics they wanted. Taking into account both practitioners' needs and current technological factors, we offer recovery of soundness through an adjusted definition of assertion validity that matches user expectations and can be implemented practically using current prover technology. We describe how support for the new semantics has been added to ESC/Java2. Preliminary results demonstrate the effectiveness of the new semantics at uncovering previously indiscernible specification errors.

Abstract The verifying compiler (VC) project proposals suggest that mainstream software developers are its targeted end-users. Like other software engineering efforts, the VC project success depends on appropriate end-user consultation. Industrial use of program assertions for the purpose of run-time assertion checking (RAC) is becoming commonplace. A likely next step on the path to VC adoption is the use of assertions in extended static checking (ESC), a fully automated form of static program verification (SPV). Unfortunately, all current VC prototypes supporting SPV, adopt a semantics which is unsound relative to the standard run-time interpretation of assertions. In this article, we report on the results of a survey in which we asked industrial developers what logical semantics they want program assertions to have, and whether consistency across RAC and SPV tools is important. Survey results indicate that developers are in favor of a semantics for assertions that is compatible with their current use in RAC.

Industrial use of program assertions for the purpose of run-time assertion checking (RAC) is becoming commonplace. A likely next step in the use of assertions is extended static checking (ESC), an area of active research that promises added benefits to industry. Unfortunately, RAC and ESC tools are not consistent in their interpretation of assertions containing undefined terms. In this paper, we report on the results of a survey in which we asked industrial developers what logical semantics they want program assertions to have, and whether consistency across tools is important. Survey results indicate that developers are in favor of a semantics for assertions that is compatible with their current use in RAC.