Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Using Graph Transformations and Graph Abstractions for Software Verification
Get PDFIn this paper we describe our intended approach for the verification of software written in imperative programming languages. We base our approach on model checking of graph transition systems, where each state is a graph and the transitions are specified by graph transformation rules. We believe that graph transformation is a very suitable technique to model the execution semantics of languages with dynamic memory allocation. Furthermore, such representation allows us to investigate the use of graph abstractions, which can mitigate the combinatorial explosion inherent to model checking. In addition to presenting our planned approach, we reason about its feasibility, and, by providing a brief comparison to other existing methods, we highlight the benefits and drawbacks that are expected
Automated Verification by Declarative Description of Graph Rewriting-Based Model Transformations
Get PDFUsually, verification of graph rewriting-based model transformations is performed manually, however, the industrial applications require automated methods. In several cases, transformation developers are interested in the offline analysis, when only the definition of the transformation and the specification of the modeling languages are taken into account. Hence, the analysis must be performed only once, and the results are independent from the concrete input models. For this purpose, transformations should be specified in a formalism that can be automatically analyzed. Based on our previous work that presented the mathematical background, this paper provides a platform-independent, declarative formalism for the specification of graph rewriting-based model transformations, and demonstrates its applicability on a case study of refactoring mobile-based social network models. Our results prove that several functional properties of the model transformations can be automatically verified, moreover, the capabilities of our methods can be extended in the future
Extending OCL Operation Contracts with Objective Functions
Get PDFWe explore the potential of adding objective functions to OCL operation contracts. If an operation contract includes an objective function, the operation has the obligation to yield results that make the objective function assume an optimal value. Thus, an objective function expresses a preference among the possible operation results that conform to the postconditions of the operation contract and any class invariants. Objective functions strictly increase the expressiveness of OCL operation contracts. While objective functions arise naturally in application domains like operations research, we argue that objective functions are a useful general-purpose specification instrument and discuss several application examples. As tool support for operation contracts with objective functions, we present an animator for OCL operation contracts with optimization capabilities. We ensure tool interoperability by specifying objective functions in a UML profile
Towards a Methodology for Semantics Specification of Domain-specific Models through Properties
Get PDFDomain-specific languages are designed for a specific domain and their use in the development of a software system enables domain experts to understand and develop models. The full description of a complex software system uses various domain-specific languages, each language having its own meaning. The definition of the precise semantics of domain-specific models is an important problem because semantics are a necessity to develop tools allowing formal analysis and verification. Current approaches focus on specific formalisms or languages which are the most appropriate to reason about certain properties. In this work we propose an approach that allows domain experts to specify the semantics of domain-specific models through properties expressed in a domain-specific language. The advantage of the approach is that domain experts can write down and understand the properties of the models
The Belgian Electronic Identity Card: a Verification Case Study
Get PDFIn the field of annotation-based source code level program verification for Java-like languages, separation-logic based verifiers offer a promising alternative to classic JML based verifiers such as ESC/Java2, the Mobius tool or Spec#. Researchers have demonstrated the advantages of separation logic based verification by showing that it is feasible to verify very challenging (though very small) sample code, such as design patterns, or highly concurrent code. However, there is little experience in using this new breed of verifiers on real code. In this paper we report on our experience of verifying several thousands of lines of Java Card code using VeriFast, one of the state-of-the-art separation logic based verifiers. We quantify annotation overhead, verification performance, and impact on code quality (number of bugs found). Finally, our experiments suggest a number of potential improvements to the VeriFast tool
Formal Modeling and Analysis for Interactive Hybrid Systems
Get PDFAn effective strategy for discovering certain kinds of automation
surprise and other problems in interactive systems is to build models
of the participating (automated and human) agents and then explore all
reachable states of the composed system looking for divergences
between mental states and those of the automation. Various kinds of
model checking provide ways to automate this approach when the agents
can be modeled as discrete automata. But when some of the agents are
continuous dynamical systems (e.g., airplanes), the composed model is
a hybrid (i.e., mixed continuous and discrete) system and these are
notoriously hard to analyze.
We describe an approach for very abstract modeling of hybrid systems
using relational approximations and their automated analysis using
infinite bounded model checking supported by an SMT solver. When
counterexamples are found, we describe how additional constraints can
be supplied to direct counterexamples toward plausible scenarios that
can be confirmed in high-fidelity simulation. The approach is
illustrated though application to a known (and now corrected)
human-automation interaction problem in Airbus aircraft
Modeling the OCL Standard Library
Get PDFOCL is widely used by UML and other languages to constrain meta-models and perform evaluations on models. The OCL specification is the result of diligent but time-constrained human endeavor and so contains many inconsistencies, most of which are relatively easy to ignore as obvious typographical mistakes. However the need to ignore minor discrepancies undermines rigorous treatment of more significant issues. The minor issues can be substantially eliminated by auto-generating the specification. This paper provides early community visibility of proposed solutions to a variety of issues that arose while developing a model for the OCL Standard Library that forms the core of the OCL specification
A Feature Model for an IDE4OCL
Get PDFAn Integrated OCL Development Environment (IDE4OCL) can significantly improve the pragmatics and practice of OCL. Therefore we started a comprehensive requirement analysis with the long term vision of a multisite IDE4OCL project. In this paper we present a feature model for the IDE4OCL vision based on this analysis. In an earlier work we identified domain concepts, tool–level interactions with IDE4OCL, and use cases for OCL developers including a set predefined features. In the second step, we asked the OCL community members for their feedback on our proposal. Around 100 researchers, tool developers and practitioners who gained experience with OCL have voted in an online–survey. The results gave us a valuable insight in the needs of OCL usage both in usual and advanced OCL applications. One of the important results is a collection of features that have been proposed additionally to our predefined features. We analysed all the comments of the participants of the survey and consolidated them into an extended set of IDE4OCL
features and eventually into a feature model