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.

Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. On the other hand, description logics (DLs) provide a well-suited formalism to describe and reason about static knowledge, used in many areas to specify domain knowledge in an ontology. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in.

By combining two of the central paradigms of causality, namely counterfactual reasoning and probability-raising,we introduce a probabilistic notion of cause in Markov chains. Such a cause consists of finite executions of the probabilistic system after which the probability of an ω-regular effect exceeds a given threshold. The cause, as a set of executions, then has to cover all behaviors exhibiting the effect. With these properties, such causes can be used for monitoring purposes where the aim is to detect faulty behavior before it actually occurs. In order to choose which cause should be computed, we introduce multiple types of costs to capture the consumption of resources by the system or monitor from different perspectives, and study the complexity of computing cost-minimal causes.

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

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.

In this thesis we focus on new methods for probabilistic model checking (PMC) with linear temporal logic (LTL). The standard approach translates an LTL formula into a deterministic ω-automaton with a double-exponential blow up. There are approaches for Markov chain analysis against LTL with exponential runtime, which motivates the search for non-deterministic automata with restricted forms of non-determinism that make them suitable for PMC. For MDPs, the approach via deterministic automata matches the double-exponential lower bound, but a practical application might benefit from approaches via non-deterministic automata. We first investigate good-for-games (GFG) automata. In GFG automata one can resolve the non-determinism for a finite prefix without knowing the infinite suffix and still obtain an accepting run for an accepted word. We explain that GFG automata are well-suited for MDP analysis on a theoretic level, but our experiments show that GFG automata cannot compete with deterministic automata. We have also researched another form of pseudo-determinism, namely unambiguity, where for every accepted word there is exactly one accepting run. We present a polynomial-time approach for PMC of Markov chains against specifications given by an unambiguous Büchi automaton (UBA). Its two key elements are the identification whether the induced probability is positive, and if so, the identification of a state set inducing probability 1. Additionally, we examine the new symbolic Muller acceptance described in the Hanoi Omega Automata Format, which we call Emerson-Lei acceptance. It is a positive Boolean formula over unconditional fairness constraints. We present a construction of small deterministic automata using Emerson-Lei acceptance. Deciding, whether an MDP has a positive maximal probability to satisfy an Emerson-Lei acceptance, is NP-complete. This fact has triggered a DPLL-based algorithm for deciding positiveness.

Computer hardware and software laid the foundation for fundamental innovations in science, technology, economics and society. Novel application areas generate an ever-increasing demand for computation power and storage capacities. Classic CMOS-based hardware and the von Neumann architecture are approaching their limits in miniaturization, power density and communication speed. To meet future demands, researchers work on new device technologies and architecture approaches which in turn require new algorithms and a hardware/software co-design to exploit their capabilities. Since the overall system heterogeneity and complexity increases, the challenge is to build systems with these technologies that are both correct and performant by design. Formal methods in general and model checking in particular are established verification methods in hardware design, and have been successfully applied to many hardware, software and integrated hardware/software systems. In many systems, probabilistic effects arise naturally, e.g., from input patterns, production variations or the occurrence of faults. Probabilistic model checking facilitates the quantitative analysis of performance and reliability measures in stochastic models that formalize this probabilism. The interdisciplinary research project Center for Advancing Electronics Dresden, cfaed for short, aims to explore hardware and software technologies for future information processing systems. It joins the research efforts of different groups working on technologies for all system layers ranging from transistor device research over system architecture up to the application layer. The collaborations among the groups showed a demand for new formal methods and enhanced tools to assist the design and analysis of technologies at all system layers and their cross-layer integration. Addressing these needs is the goal of this thesis. This work contributes to probabilistic model checking for Markovian models with new methods to compute two essential measures in the analysis of hardware/software systems and a method to tackle the state-space explosion problem: 1) Conditional probabilities are well known in stochastic theory and statistics, but efficient methods did not exist to compute conditional expectations in Markov chains and extremal conditional probabilities in Markov decision processes. This thesis develops new polynomial-time algorithms, and it provides a mature implementation for the probabilistic model checker PRISM. 2) Relativized long-run and relativized conditional long-run averages are proposed in this work to reason about probabilities and expectations in Markov chains on the long run when zooming into sets of states or paths. Both types of long-run averages are implemented for PRISM. 3) Symmetry reduction is an effective abstraction technique to tame the state-space explosion problem. However, state-of-the-art probabilistic model checkers apply it only after building the full model and offer no support for specifying non-trivial symmetric components. This thesis fills this gap with a modeling language based on symmetric program graphs that facilitates symmetry reduction on the source level. The new language can be integrated seamlessly into the PRISM modeling language. This work contributes to the research on future hardware/software systems in cfaed with three practical studies that are enabled by the developed methods and their implementations. 1) To confirm relevance of the new methods in practice and to validate the results, the first study analyzes a well-understood synchronization protocol, a test-and-test-and-set spinlock. Beyond this confirmation, the analysis demonstrates the capability to compute properties that are hardly accessible to measurements. 2) Probabilistic write-copy/select is an alternative protocol to overcome the scalability issues of classic resource-locking mechanisms. A quantitative analysis verifies the protocol's principle of operation and evaluates the performance trade-offs to guide future implementations of the protocol. 3) The impact of a new device technology is hard to estimate since circuit-level simulations are not available in the early stages of research. This thesis proposes a formal framework to model and analyze circuit designs for novel transistor technologies. It encompasses an operational model of electrical circuits, a functional model of polarity-controllable transistor devices and algorithms for design space exploration in order to find optimal circuit designs using probabilistic model checking. A practical study assesses the model accuracy for a lab-device based on germanium nanowires and performs an automated exploration and performance analysis of the design space of a given switching function. The experiments demonstrate how the framework enables an early systematic design space exploration and performance evaluation of circuits for experimental transistor devices.:1. Introduction 1.1 Related Work 2. Preliminaries 3. Conditional Probabilities in Markovian Models 3.1 Methods for Discrete- and Continuous-Time Markov Chains 3.2 Reset Method for Markov Decision Processes 3.3 Implementation 3.4 Evaluation and Comparative Studies 3.5 Conclusion 4. Long-Run Averages in Markov Chains 4.1 Relativized Long-Run Average 4.2 Conditional State Evolution 4.3 Implementation 4.4 Conclusion 5. Language-Support for Immediate Symmetry Reduction 5.1 Probabilistic Program Graphs 5.2 Symmetric Probabilistic Program Graphs 5.3 Implementation 5.4 Conclusion 6. Practical Applications of the Developed Techniques 6.1 Test-and-Test-and-Set Spinlock: Quantitative Analysis of an Established Protocol 6.2 Probabilistic Write/Copy-Select: Quantitative Analysis as Design Guide for a Novel Protocol 6.3 Circuit Design for Future Transistor Technologies: Evaluating Polarity-Controllable Multiple-Gate FETs 7. Conclusion Bibliography Appendices A. Conditional Probabilities and Expectations A.1 Selection of Benchmark Models A.2 Additional Benchmark Results A.3 Comparison PRISM vs. Storm B. Language-Support for Immediate Symmetry Reduction B.1 Syntax of the PRISM Modeling Language B.2 Multi-Core Example C. Practical Applications of the Developed Techniques C.1 Test-and-Test-and-Set Spinlock C.2 Probabilistic Write/Copy-Select C.3 Circuit Design for Future Transistor Technologies

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.

The topic of this paper is the determinization problem of ω-automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.