A reactive control system is a computer system reacting to certain stimuli emitted by its environment in order to maintain it in a desired state. Distributed reactive control systems are generally composed of several processes, running in parallel on one or more computers, communicating with one another to perform the required control task. By their very nature, distributed reactive control systems are hard to design. Their distributed nature and/or the communication scheme used can introduce subtle unforeseen behaviours. When dealing with critical applications, such as plane control systems, or traffic light control systems, those unintended behaviours can have disastrous consequences. It is therefore essential, for the designer, to ensure that this does not happen. For that purpose, rigorous and systematic techniques can (and should) be applied as early as possible in the development process. In that spirit, this work aims at providing the designer with the necessary tools in order to facilitate the development and validation of such distributed reactive control systems. In particular, we show how using a dedicated language called dSL (Distributed Supervision language) can be used to ease the development process. We also study how validations techniques such as model-checking and testing can be applied in this context. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Stateless model checking is a technique for testing and verifying concurrent programs, based on exploring the different ways in which operations executed by the processes of a concurrent program can be scheduled. The goal of the technique is to expose all behaviours that can be a result of scheduling non-determinism. As the number of possible schedulings is huge, however, techniques that reduce the number of schedulings that must be explored to achieve verification have been developed. Dynamic partial order reduction (DPOR) is a prominent such technique. This dissertation presents a number of improvements to dynamic partial order reduction that significantly increase the effectiveness of stateless model checking. Central among these improvements are the Source and Optimal DPOR algorithms (and the theoretical framework behind them) and a technique that allows the observability of the interference of operations to be used in dynamic partial order reduction. Each of these techniques can exponentially decrease the number of schedulings that need to be explored to verify a concurrent program. The dissertation also presents a simple bounding technique that is compatible with DPOR algorithms and effective for finding bugs in concurrent programs, if the number of schedulings is too big to make full verification possible in a reasonable amount of time, even when the improved algorithms are used. All improvements have been implemented in Concuerror, a tool for applying stateless model checking to Erlang programs. In order to increase the effectiveness of the tool, the interference of the high-level operations of the Erlang/OTP implementation is examined, classified and precisely characterized. Aspects of the implementation of the tool are also described. Finally, a use case is presented, showing how Concuerror was used to find bugs and verify key correctness properties in repair techniques for the CORFU chain replication protocol. / UPMARC / RELEASE

The aim of the masters thesis is to design and implement a tool for automatic generation of paths in source code. Firstly was acquired a study of model based testing and possible design for the desired automatic generator based on coverage criteria defined on CFG model. The main point of the master theis is the tool design and description of its implementation. The tool supports many coverage criteria, which allows the user of such tool to focus on specific artefact of the system under test. Moreover, this tool is tuned to allow aditional requirements on the size of generated test suite, reflecting real world practical usage. The generator was implemented in C++ language and web interface for it in Python language, which at the same time is used to integrated the tool into Testos platform.

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.

The local false discovery rate (LFDR) is one of many existing statistical methods that analyze multiple hypothesis testing. As a Bayesian quantity, the LFDR is based on the prior probability of the null hypothesis and a mixture distribution of null and non-null hypothesis. In practice, the LFDR is unknown and needs to be estimated. The empirical Bayes approach can be used to estimate that mixture distribution. Empirical Bayes does not require complete information about the prior and hyper prior distributions as in hierarchical Bayes. When we do not have enough information at the prior level, and instead of placing a distribution at the hyper prior level in the hierarchical Bayes model, empirical Bayes estimates the prior parameters using the data via, often, the marginal distribution. In this research, we developed new Bayesian methods under unknown prior distribution. A set of adequate prior distributions maybe defined using Bayesian model checking by setting a threshold on the posterior predictive p-value, prior predictive p-value, calibrated p-value, Bayes factor, or integrated likelihood. We derive a set of adequate posterior distributions from that set. In order to obtain a single posterior distribution instead of a set of adequate posterior distributions, we used a blended distribution, which minimizes the relative entropy of a set of adequate prior (or posterior) distributions to a "benchmark" prior (or posterior) distribution. We present two approaches to generate a blended posterior distribution, namely, updating-before-blending and blending-before-updating. The blended posterior distribution can be used to estimate the LFDR by considering the nonlocal false discovery rate as a benchmark and the different LFDR estimators as an adequate set. The likelihood ratio can often be misleading in multiple testing, unless it is supplemented by adjusted p-values or posterior probabilities based on sufficiently strong prior distributions. In case of unknown prior distributions, they can be estimated by empirical Bayes methods or blended distributions. We propose a general framework for applying the laws of likelihood to problems involving multiple hypotheses by bringing together multiple statistical models. We have applied the proposed framework to data sets from genomics, COVID-19 and other data.

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

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche. / Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis.

Model checking problems suffer from state space explosion. State space explosion is the number of states in the graph increases exponentially with the number of variables in the state description. Searching the large graphs required in model checking requires an efficient algorithm. This dissertation explores several methods to improve an externalmemory search algorithm for model checking problems. A tool implementing these methods is built on top of the Murphi model checker. One improvement is a state cache for immediate detection leveraging the properties of state locality. A novel type of locality, intralayer locality is explained and shown to exist in a variety of search spaces. Another improvement, partial delayed duplicate detection, exploits interlayer locality to reduce search times. An automatic partitioning function is described that allows hash-based delayed duplicate detection to be used without domain knowledge of the state space. A phased delayed duplicate detection algorithm combining features of hash-based delayed duplicate detection and sorting-based delayed duplicate detection is explained and compared to the other methods.

yes / This Workshop on Membrane Computing, at the Conference of Unconventional Computation and Natural Computation (UCNC), 12th July 2016, Manchester, UK, is the second event of this type after the Workshop at UCNC 2015 in Auckland, New Zealand*. Following the tradition of the 2015 Workshop the Proceedings are published as technical report. The Workshop consisted of one invited talk and six contributed presentations (three full papers and three extended abstracts) covering a broad spectrum of topics in Membrane Computing, from computational and complexity theory to formal verification, simulation and applications in robotics. All these papers – see below, but the last extended abstract, are included in this volume. The invited talk given by Rudolf Freund, “P SystemsWorking in Set Modes”, presented a general overview on basic topics in the theory of Membrane Computing as well as new developments and future research directions in this area. Radu Nicolescu in “Distributed and Parallel Dynamic Programming Algorithms Modelled on cP Systems” presented an interesting dynamic programming algorithm in a distributed and parallel setting based on P systems enriched with adequate data structure and programming concepts representation. Omar Belingheri, Antonio E. Porreca and Claudio Zandron showed in “P Systems with Hybrid Sets” that P systems with negative multiplicities of objects are less powerful than Turing machines. Artiom Alhazov, Rudolf Freund and Sergiu Ivanov presented in “Extended Spiking Neural P Systems with States” new results regading the newly introduced topic of spiking neural P systems where states are considered. “Selection Criteria for Statistical Model Checker”, by Mehmet E. Bakir and Mike Stannett, presented some early experiments in selecting adequate statistical model checkers for biological systems modelled with P systems. In “Towards Agent-Based Simulation of Kernel P Systems using FLAME and FLAME GPU”, Raluca Lefticaru, Luis F. Macías-Ramos, Ionuţ M. Niculescu, Laurenţiu Mierlă presented some of the advatages of implementing kernel P systems simulations in FLAME. Andrei G. Florea and Cătălin Buiu, in “An Efficient Implementation and Integration of a P Colony Simulator for Swarm Robotics Applications" presented an interesting and efficient implementation based on P colonies for swarms of Kilobot robots. *http://ucnc15.wordpress.fos.auckland.ac.nz/workshop-on-membrane-computingwmc- at-the-conference-on-unconventional-computation-natural-computation/

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.