A formal verification technique for behavioural model-to-model transformations
In Model Driven Software Engineering, models and model transformations are the primary artifacts when developing a software system. In such a workflow, model transformations are used to incrementally transform initial abstract models into concrete ...
ProFeat: feature-oriented engineering for family-based probabilistic model checking
The concept of features provides an elegant way to specify families of systems. Given a base system, features encapsulate additional functionalities that can be activated or deactivated to enhance or restrict the base system’s behaviors. Features ...
Model-based testing of probabilistic systems
This work presents an executable model-based testing framework for probabilistic systems with non-determinism. We provide algorithms to automatically generate, execute and evaluate test cases from a probabilistic requirements specification. The ...
Cut branches before looking for bugs: certifiably sound verification on relaxed slices
Program slicing can be used to reduce a given initial program to a smaller one (a slice) that preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&V) of software can become easier on ...
Variability-based model transformation: formal foundation and application
Model transformation systems often contain transformation rules that are substantially similar to each other, causing maintenance issues and performance bottlenecks. To address these issues, we introduce variability-based model transformation. The ...
A semantics comparison workbench for a concurrent, asynchronous, distributed programming language
A number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time—...