The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one way to tackle the challenging state explosion problem, PRISM supports symbolic storage and manipulation using multi-terminal binary decision diagrams for representing the models and in the computations. However, it lacks automated heuristics for variable reordering, even though it is well known that the order of BDD variables plays a crucial role for compact representations and efficient computations. In this article, we present a collection of extensions to PRISM. First, we provide support for automatic variable reordering within the symbolic engines of PRISM and allow users to manually control the variable ordering at a fine-grained level. Second, we provide extensions in the realm of reward-bounded properties, namely symbolic computations of quantiles in Markov decision processes and, for both the explicit and symbolic engines, the approximative computation of quantiles for continuous-time Markov chains as well as support for multi-reward-bounded properties. Finally, we provide an implementation for obtaining minimal weak deterministic Büchi automata for the obligation fragment of linear temporal logic (LTL), with applications for expected accumulated reward computations with a finite horizon given by a co-safe LTL formula.

For modeling and reasoning about complex systems, symbolic methods provide a prominent way to tackle the state explosion problem. It is well known that for symbolic approaches based on binary decision diagrams (BDD), the ordering of BDD variables plays a crucial role for compact representations and efficient computations. We have extended the popular probabilistic model checker PRISM with support for automatic variable reordering in its multi-terminal-BDD-based engines and report on benchmark results. Our extensions additionally allow the user to manually control the variable ordering at a finer-grained level. Furthermore, we present our implementation of the symbolic computation of quantiles and support for multi-reward-bounded properties, automata specifications and accepting end component computations for Streett conditions.

We present an extension of the popular probabilistic model checker PRISM with multi-actions that enables the modeling of complex coordination between stochastic components in an exogenous manner. This is supported by tooling that allows the use of the exogenous coordination language Reo for specifying the coordination glue code. The tool provides an automatic compilation feature for translating a Reo network of channels into PRISM's guarded command language. Additionally, the tool supports the translation of reward monitoring components that can be attached to the Reo network to assign rewards or cost to activity within the coordination network. The semantics of the translated model is then based on weighted Markov decision processes that yield the basis, e.g., for a quantitative analysis using PRISM. Feasibility of the approach is shown by a quantitative analysis of an energy-aware network system example modeled with a role-based modeling approach in Reo.

The concept of roles is a promising approach to cope with context dependency and adaptivity of modern software systems. While roles have been investigated in conceptual modeling, programming languages and multi-agent systems, they have been given little consideration within component-based systems. In this paper, we propose a hierarchical role-based approach for modeling relationships and collaborations between components. In particular, we consider the channel-based, exogenous coordination language Reo and discuss possible realizations of roles and related concepts. The static requirements on the binding of roles are modeled by rule sets expressed in many-sorted second-order logic and annotations on the Reo networks for role binding, context and collaborations, while Reo connectors are used to model the coordination of runtime role playing. The ideas presented in this paper may serve as a basis for the formalization and formal analysis of role-based software systems.

Heutzutage besteht ein komplexes Software-System häufig aus lose gekoppelten, interagierenden Komponenten. Eine Komponente ist ein offenes System, das unabhängig von anderen offenen Systemen entwickelt und später mit diesen komponiert wird. Die Komposition L+R zweier offener Systeme L und R kann sich jedoch inkorrekt verhalten, beispielsweise verklemmen (die Komponenten warten gegenseitig aufeinander), in eine Endlosschleife geraten oder unbeschränkten Speicherplatz erfordern. Ist L+R dagegen ein korrektes System, bezeichnet man L und R als Partner voneinander. Formale Methoden der Modellierung, Analyse und Synthese ermöglichen die systematische Konstruktion eines korrekten Systems durch Komposition von Partnern. Die Kosten, die ein offenes System L verursacht, variieren in Abhängigkeit von der konkreten Wahl eines Partners. Es ist daher wünschenswert, L nur mit solchen Partnern zu komponieren, welche die Kosten von L beschränken oder sogar minimieren. Ein Partner, der die Kosten von L minimiert, ist ein optimaler Partner von L. Ziel dieser Arbeit ist die Erarbeitung von Techniken, die garantieren, dass L nur mit optimalen Partnern komponiert wird. Dazu entwickeln wir formale Methoden zur Modellierung, Analyse und Synthese kostenbehafteter offener Systeme und ihrer optimalen Partner. Wir präsentieren einen Formalismus zur Modellierung funktionaler (d.h. Zustandsübergänge) und nicht-funktionaler Verhaltenseigenschaften (d.h. Kosten). In diesem Formalismus definieren wir Kostenbeschränktheit und Optimalität von Partnern. Darauf aufbauend entwickeln wir formale Methoden zur Entscheidung der kostenbeschränkten Bedienbarkeit (d.h. der Existenz kostenbeschränkter Partner), der Synthese optimaler Partner und der endlichen Repräsentation aller optimalen Partner. / Nowadays, a complex software system usually consists of loosely-coupled, interacting components. Such a component is an independently developed open system that one composes with other open systems. The composition L+R of two open systems L and R can be faulty: For instance, the components deadlock (i.e. mutually wait for each other) or require an unbounded amount of memory. If L+R is correct, L and R are called partners of each other. Formal methods for modeling, analysis and synthesis yield a systematic approach to constructing a correct system by means of composing partners. The costs of executing a given open system L vary based on a chosen partner. Therefore, it is desirable to choose a partner that bounds or even minimizes the costs of executing L. If a partner R minimizes the costs of executing L, then R is an optimal partner of L. Our goal is to develop techniques that guarantee the composition of L with optimal partners. To this end, we develop formal methods of modeling, analysis and synthesis of open systems incorporating costs. We present a formalism to model functional aspects (i.e. states and transitions) and non-functional aspects (costs) of behavior. We define the properties of cost boundedness and cost optimality for partners in this formalism. Based thereon, we develop formal methods to decide cost bounded controllability (i.e. the existence of cost bounded partners), to synthesize optimal partners, and to finitely represent the set of all optimal partners.

With the widespread use of information systems in modern society comes a growing demand for customizable and adaptable software. As a result, systems are increasingly developed as families of products adapted to specific contexts and requirements. Features are an established concept to capture the commonalities and variability between system variants. Most prominently, the concept is applied in the design, modeling, analysis, and implementation of software product lines where products are built upon a common base and are distinguished by their features. While adaptations encapsulated within features are mainly static and remain part of the system after deployment, dynamic adaptations become increasingly important. Especially interconnected mobile devices and embedded systems are required to be context-sensitive and (self-)adaptive. A promising concept for the design and implementation of such systems are roles as they capture context-dependent and collaboration-specific behavior. A major challenge in the development of feature-oriented and role-based systems are interactions, i.e., emergent behavior that arises from the combination of multiple features or roles. As the number of possible combinations is usually exponential in the number of features and roles, the detection of such interactions is difficult. Since unintended interactions may compromise the functional correctness of a system and may lead to reduced efficiency or reliability, it is desirable to detect them as early as possible in the development process. The goal of this thesis is to adopt the concepts of features and roles in the formal modeling and analysis of systems and system families. In particular, the focus is on the quantitative analysis of operational models by means of probabilistic model checking for supporting the development process and for ensuring correctness. The tool ProFeat, which enables a quantitative analysis of stochastic system families defined in terms of features, has been extended with additional language constructs, support for a one-by-one analysis of system variants, and a symbolic representation of analysis results. The implementation is evaluated by means of several case studies which compare different analysis approaches and show how ProFeat facilitates a family-based quantitative analysis of systems. For the compositional modeling of role-based systems, role-based automata (RBA) are introduced. The thesis presents a modeling language that is based on the input language of the probabilistic model checker PRISM to compactly describe RBA. Accompanying tool support translates RBA models into the PRISM language to enable the formal analysis of functional and non-functional properties, including system dynamics, contextual changes, and interactions. Furthermore, an approach for a declarative and compositional definition of role coordinators based on the exogenous coordination language Reo is proposed. The adequacy of the RBA approach for detecting interactions within context-sensitive and adaptive systems is shown by several case studies.:1 Introduction 1.1 Engineering approaches for variant-rich adaptive systems 1.2 Validation and verification methods 1.3 Analysis of feature-oriented and role-based systems 1.4 Contribution 1.5 Outline 2 Preliminaries I Feature-oriented systems 3 Feature-oriented engineering for family-based analysis 3.1 Feature-oriented development 3.2 Describing system families: The ProFeat language 3.2.1 Feature-oriented language constructs 3.2.2 Parametrization 3.2.3 Metaprogramming language extensions 3.2.4 Property specifications 3.2.5 Semantics 3.3 Implementation 3.3.1 Translation of ProFeat models 3.3.2 Post-processing of analysis results 4 Case studies and application areas 4.1 Comparing family-based and product-based analysis 4.1.1 Analysis of feature-oriented systems 4.1.2 Analysis of parametrized systems 4.2 Software product lines 4.2.1 Body sensor network 4.2.2 Elevator product line 4.3 Self-adaptive systems 4.3.1 Adaptive network system model 4.3.2 Adaptation protocol for distributed systems II Role-based Systems 5 Formal modeling and analysis of role-based systems 5.1 The role concept 5.1.1 Towards a common notion of roles 5.1.2 The Compartment Role Object Model 5.1.3 Roles in programming languages 5.2 Compositional modeling of role-based behavior 5.2.1 Role-based automata and their composition 5.2.2 Algebraic properties of compositions 5.2.3 Coordination and semantics of RBA 6 Implementation of a role-oriented modeling language 6.1 Role-oriented modeling language 6.1.1 Declaration of the system structure 6.1.2 Definition of operational behavior 6.2 Translation of role-based models 6.2.1 Transformation to multi-action MDPs 6.2.2 Multi-action extension of PRISM 6.2.3 Translation of components 6.2.4 Translation of role-playing coordinators 6.2.5 Encoding role-playing into states 7 Exogenous coordination of roles 7.1 The exogenous coordination language Reo 7.2 Constraint automata 7.3 Embedding of role-based automata in constraint automata 7.4 Implementation 7.4.1 Exogenous coordination of PRISM modules 7.4.2 Reo for exogenous coordination within PRISM 8 Evaluation of the role-oriented approach 8.1 Experimental studies 8.1.1 Peer-to-peer file transfer 8.1.2 Self-adaptive production cell 8.1.3 File transfer with exogenous coordination 8.2 Classification 8.3 Related work 8.3.1 Role-based approaches 8.3.2 Aspect-oriented approaches 8.3.3 Feature-oriented approaches 9 Conclusion

Immer wenn neue Anforderungen an ein System gestellt werden, müssen die Korrektheit und Konsistenz der Systemspezifikation überprüft werden, was in der Praxis in der Regel manuell erfolgt. Eine mögliche Option, um die Nachteile dieser manuellen Analyse zu überwinden, ist das sogenannte Contract-Based Design. Dieser Entwurfsansatz kann den Verifikationsprozess zur Überprüfung, ob die Anforderungen auf oberster Ebene konsistent verfeinert wurden, automatisieren. Die Verifikation kann somit iterativ durchgeführt werden, um die Korrektheit und Konsistenz des Systems angesichts jeglicher Änderung der Spezifikationen sicherzustellen. Allerdings ist es aufgrund der mangelnden Benutzerfreundlichkeit und der Schwierigkeiten bei der Interpretation von Verifizierungsergebnissen immer noch eine Herausforderung, formale Ansätze in der Industrie einzusetzen. Stellt beispielsweise der Model Checker bei der Verifikation eine Inkonsistenz fest, generiert er ein Gegenbeispiel (Counterexample) und weist gleichzeitig darauf hin, dass die gegebenen Eingabespezifikationen inkonsistent sind. Hier besteht die gewaltige Herausforderung darin, das generierte Gegenbeispiel zu verstehen, das oft sehr lang, kryptisch und komplex ist. Darüber hinaus liegt es in der Verantwortung der Ingenieurin bzw. des Ingenieurs, die inkonsistente Spezifikation in einer potenziell großen Menge von Spezifikationen zu identifizieren. Diese Arbeit schlägt einen Ansatz zur Erklärung von Gegenbeispielen (Counterexample Explanation Approach) vor, der die Verwendung von formalen Methoden vereinfacht und fördert, indem benutzerfreundliche Erklärungen der Verifikationsergebnisse der Ingenieurin bzw. dem Ingenieur präsentiert werden. Der Ansatz zur Erklärung von Gegenbeispielen wird mittels zweier Methoden evaluiert: (1) Evaluation anhand verschiedener Anwendungsbeispiele und (2) eine Benutzerstudie in Form eines One-Group Pretest-Posttest Experiments. / Whenever new requirements are introduced for a system, the correctness and consistency of the system specification must be verified, which is often done manually in industrial settings. One viable option to traverse disadvantages of this manual analysis is to employ the contract-based design, which can automate the verification process to determine whether the refinements of top-level requirements are consistent. Thus, verification can be performed iteratively to ensure the system’s correctness and consistency in the face of any change in specifications. Having said that, it is still challenging to deploy formal approaches in industries due to their lack of usability and their difficulties in interpreting verification results. For instance, if the model checker identifies inconsistency during the verification, it generates a counterexample while also indicating that the given input specifications are inconsistent. Here, the formidable challenge is to comprehend the generated counterexample, which is often lengthy, cryptic, and complex. Furthermore, it is the engineer’s responsibility to identify the inconsistent specification among a potentially huge set of specifications. This PhD thesis proposes a counterexample explanation approach for formal methods that simplifies and encourages their use by presenting user-friendly explanations of the verification results. The proposed counterexample explanation approach identifies and explains relevant information from the verification result in what seems like a natural language statement. The counterexample explanation approach extracts relevant information by identifying inconsistent specifications from among the set of specifications, as well as erroneous states and variables from the counterexample. The counterexample explanation approach is evaluated using two methods: (1) evaluation with different application examples, and (2) a user-study known as one-group pretest and posttest experiment.

Informationssysteme verarbeiten Daten, die logisch und physisch über Knoten verteilt sind. Datenobjekte verschiedener Knoten können dabei Bezüge zueinander haben. Beispielsweise kann ein Datenobjekt eine Referenz auf ein Datenobjekt eines anderen Knotens oder eine kritische Information enthalten. Die Semantik der Daten induziert Datenintegrität in Form von Anforderungen: Zum Beispiel sollte keine Referenz verwaist und kritische Informationen nur an einem Knoten verfügbar sein. Datenintegrität unterscheidet gültige von ungültigen Verteilungen der Daten. Ein verteiltes System verändert sich in Schritten, die nebenläufig auftreten können. Jeder Schritt manipuliert Daten. Ein verteiltes System erhält Datenintegrität, wenn alle Schritte in einer Datenverteilung resultieren, die die Anforderungen von Datenintegrität erfüllen. Die Erhaltung von Datenintegrität ist daher ein notwendiges Korrektheitskriterium eines Systems. Der Entwurf und die Analyse von Datenintegrität in verteilten Systemen sind schwierig, weil ein verteiltes System nicht global kontrolliert werden kann. In dieser Arbeit untersuchen wir formale Methoden für die Modellierung und Analyse verteilter Systeme, die mit Daten arbeiten. Wir entwickeln die Grundlagen für die Verifikation von Systemmodellen. Dazu verwenden wir algebraische Petrinetze. Wir zeigen, dass die Schritte verteilter Systeme mit endlichen vielen Transitionen eines algebraischen Petrinetzes beschrieben werden können, genau dann, wenn eine Schranke für die Bedingungen aller Schritte existiert. Wir verwenden algebraische Gleichungen und Ungleichungen, um Datenintegrität zu spezifizieren. Wir zeigen, dass die Erhaltung von Datenintegrität unentscheidbar ist, wenn alle erreichbaren Schritte betrachtet werden. Und wir zeigen, dass die Erhaltung von Datenintegrität entscheidbar ist, wenn auch unerreichbare Schritte berücksichtigt werden. Dies zeigen wir, indem wir die Berechenbarkeit eines nicht-erhaltenden Schrittes als Zeugen zeigen. / Information systems process data that is logically and physically distributed over many locations. Data entities at different locations may be in a specific relationship. For example, a data entity at one location may contain a reference to a data entity at a different location, or a data entity may contain critical information such as a password. The semantics of data entities induce data integrity in the form of requirements. For example, no references should be dangling, and critical information should be available at only one location. Data integrity discriminates between correct and incorrect data distributions. A distributed system progresses in steps, which may occur concurrently. In each step, data is manipulated. Each data manipulation is performed locally and affects a bounded number of data entities. A distributed system preserves data integrity if each step of the system yields a data distribution that satisfies the requirements of data integrity. Preservation of data integrity is a necessary condition for the correctness of a system. Analysis and design are challenging, as distributed systems lack global control, employ different technologies, and data may accumulate unboundedly. In this thesis, we study formal methods to model and analyze distributed data-aware systems. As a result, we provide a technology-independent framework for design-time analysis. To this end, we use algebraic Petri nets. We show that there exists a bound for the conditions of each step of a distributed system if and only if the steps can be described by a finite set of transitions of an algebraic Petri net. We use algebraic equations and inequalities to specify data integrity. We show that preservation of data integrity is undecidable in case we consider all reachable steps. We show that preservation of data integrity is decidable in case we also include unreachable steps. We show the latter by showing computability of a non-preserving step as a witness.

Feature-based formalisms provide an elegant way to specify families of systems that share a base functionality and differ in certain features. They can also facilitate an all-in-one analysis, where all systems of the family are analyzed at once on a single family model instead of one-by-one. This paper presents the basic concepts of the tool ProFeat, which provides a guarded-command language for modeling families of probabilistic systems and an automatic translation of family models to the input language of the probabilistic model checker PRISM. This translational approach enables a family-based quantitative analysis with PRISM. Besides modeling families of systems that differ in system parameters such as the number of identical processes or channel sizes, ProFeat also provides special support for the modeling and analysis of (probabilistic) product lines with dynamic feature switches, multi-features and feature attributes. By means of several case studies we show how ProFeat eases family-based modeling and compare the one-by-one and all-in-one analysis approach.

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 can also facilitate the analysis of families of systems by exploiting commonalities of the family members and performing an all-in-one analysis, where all systems of the family are analyzed at once on a single family model instead of one-by-one. Most prominent, the concept of features has been successfully applied to describe and analyze (software) product lines. We present the tool ProFeat that supports the feature-oriented engineering process for stochastic systems by probabilistic model checking. To describe families of stochastic systems, ProFeat extends models for the prominent probabilistic model checker Prism by feature-oriented concepts, including support for probabilistic product lines with dynamic feature switches, multi-features and feature attributes. ProFeat provides a compact symbolic representation of the analysis results for each family member obtained by Prism to support, e.g., model repair or refinement during feature-oriented development. By means of several case studies we show how ProFeat eases family-based quantitative analysis and compare one-by-one and all-in-one analysis approaches.