DNA nanotechnology is a rapidly developing field that creates nanoscale devices from DNA, which enables novel interfaces with biological material. Their therapeutic use is envisioned and applications in other areas of basic science have already been found. These devices function at physiological conditions and, owing to their molecular scale, are subject to thermal fluctuations during both preparation and operation of the device. Troubleshooting a failed device is often difficult and we develop models to characterise two separate devices: DNA walkers and DNA origami. Our framework is that of continuous-time Markov chains, abstracting away much of the underlying physics. The resulting models are coarse but enable analysis of system-level performance, such as ‘the molecular computation eventually returns the correct answer with high probability’. We examine the applicability of probabilistic model checking to provide guarantees on the behaviour of nanoscale devices, and to this end we develop novel model checking methodology. We model a DNA walker that autonomously navigates a series of junctions, and we derive design principles that increase the probability of correct computational output. We also develop a novel parameter synthesis method for continuous-time Markov chains, for which the synthesised models guarantee a predetermined level of performance. Finally, we develop a novel discrete stochastic assembly model of DNA origami from first principles. DNA origami is a widespread method for creating nanoscale structures from DNA. Our model qualitatively reproduces experimentally observed behaviour and using the model we are able to rationally steer the folding pathway of a novel polymorphic DNA origami tile, controlling the eventual shape.

Les travaux développés dans cette thèse visent à assister le processus d’ingénierie des exigences temporelles pour les systèmes complexes à contraintes de temps. Nos contributions portent sur trois volets : la spécification des exigences, la modélisation du comportement et la vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Ensuite, afin de cadrer l’utilisateur durant l’expression des exigences, une grammaire de spécification à base de motifs prédéfinis en langage naturel est développée. Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantie pas la cohérence de l’ensemble des exigences exprimées. Ainsi, nous avons développé des mécanismes capables de détecter certains types d’incohérences entre les exigences temporelles. Pour le volet modélisation du comportement, nous avons proposé un algorithme de transformation des state-machine avec des annotations temporelles en des automates temporisés. L’idée étant de manipuler une notation assez intuitive et de générer automatiquement des modèles formels qui se prêtent à la vérification. Finalement, pour le volet vérification, nous avons adopté une technique de vérification à base d’observateurs et qui repose sur le model-checking. Concrètement, nous avons élaboré une base de patterns d’observation (ou observateurs) ; chacun des patterns développés est relatif à un type d’exigence temporelle dans la nouvelle classification. Ainsi, la vérification est réduite à une analyse d’accessibilité des états correspondants à la violation de l’exigence associée / The work developed in this thesis aims to assist the engineering process of temporal requirements for time-constrained complex systems. Our contributions concern three phases: the specification, the behaviour modelling and the verification. For the specification of temporal requirements, a new temporal properties typology taking into account all the common requirements one may meet when dealing with requirements specification, is introduced. Then, to facilitate the expression, we have proposed a structured English grammar. Nevertheless, even if each requirement taken individually is correct, we have no guarantee that a set of temporal properties one may express is consistent. Here we have proposed an algorithm based on graph theory techniques to check the consistency of temporal requirements sets. For the behaviour modelling, we have proposed an algorithm for transforming UML State Machine with time annotations into Timed Automata (TA). The idea is to allow the user manipulating a quite intuitive notation (UML SM diagramsduring the modelling phase and thereby, automatically generate formal models (TA) that could be used directly by the verification process. Finally, for the verification phase, we have adopted an observer-based technique. Actually, we have developed a repository of observation patterns where each pattern is relative to a particular temporal requirement class in our classification. Thereby, the verification process is reduced to a reachability analysis of the observers’ KO states relatives to the requirements’ violation

<P align="justify">Model-checking is an automated technique which aims at verifying properties of computer systems. A model-checker is fed with a model of the system (which capture all its possible behaviors) and a property to verify on this model. Both are given by a convenient mathematical formalism like, for instance, a transition system for the model and a temporal logic formula for the property.</P><p><p><P align="justify">For several reasons (the model-checking is undecidable for this class of model or the model-checking needs too much resources for this model) model-checking may not be applicable. For safety properties (which basically says "nothing bad happen"), a solution to this problem uses a simpler model for which model-checkers might terminate without too much resources. This simpler model, called the abstract model, over-approximates the behaviors of the concrete model. However the abstract model might be too imprecise. In fact, if the property is true on the abstract model, the same holds on the concrete. On the contrary, when the abstract model violates the property, either the violation is reproducible on the concrete model and so we found an error; or it is not reproducible and so the model-checker is said to be inconclusive. Inconclusiveness stems from the over-approximation of the concrete model by the abstract model. So a precise model yields the model-checker to conclude, but precision comes generally with an increased computational cost.</P><p><p><P align="justify">Recently, a lot of work has been done to define abstraction refinement algorithms. Those algorithms compute automatically abstract models which are refined as long as the model-checker is inconclusive. In the thesis, we give a new abstraction refinement algorithm which applies for safety properties. We compare our algorithm with previous attempts to build abstract models automatically and show, using formal proofs that our approach has several advantages. We also give several extensions of our algorithm which allow to integrate existing techniques used in model-checking such as acceleration techniques.</P><p><p><P align="justify">Following a rigorous methodology we then instantiate our algorithm for a variety of models ranging from finite state transition systems to infinite state transition systems. For each of those models we prove the instantiated algorithm terminates and provide encouraging preliminary experimental results.</P><p><br><p><br><p><P align="justify">Le model-checking est une technique automatisée qui vise à vérifier des propriétés sur des systèmes informatiques. Les données passées au model-checker sont le modèle du système (qui en capture tous les comportements possibles) et la propriété à vérifier. Les deux sont donnés dans un formalisme mathématique adéquat tel qu'un système de transition pour le modèle et une formule de logique temporelle pour la propriété.</P><p><p><P align="justify">Pour diverses raisons (le model-checking est indécidable pour cette classe de modèle ou le model-checking nécessite trop de ressources pour ce modèle) le model-checking peut être inapplicable. Pour des propriétés de sûreté (qui disent dans l'ensemble "il ne se produit rien d'incorrect"), une solution à ce problème recourt à un modèle simplifié pour lequel le model-checker peut terminer sans trop de ressources. Ce modèle simplifié, appelé modèle abstrait, surapproxime les comportements du modèle concret. Le modèle abstrait peut cependant être trop imprécis. En effet, si la propriété est vraie sur le modèle abstrait alors elle l'est aussi sur le modèle concret. En revanche, lorsque le modèle abstrait enfreint la propriété :soit l'infraction peut être reproduite sur le modèle concret et alors nous avons trouvé une erreur ;soit l'infraction ne peut être reproduite et dans ce cas le model-checker est dit non conclusif. Ceci provient de la surapproximation du modèle concret faite par le modèle abstrait. Un modèle précis aboutit donc à un model-checking conclusif mais son coût augmente avec sa précision.</P><p><P align="justify">Récemment, différents algorithmes d'abstraction raffinement ont été proposés. Ces algorithmes calculent automatiquement des modèles abstraits qui sont progressivement raffinés jusqu'à ce que leur model-checking soit conclusif. Dans la thèse, nous définissons un nouvel algorithme d'abstraction raffinement pour les propriétés de sûreté. Nous comparons notre algorithme avec les algorithmes d'abstraction raffinement antérieurs. A l'aide de preuves formelles, nous montrons les avantages de notre approche. Par ailleurs, nous définissons des extensions de l'algorithme qui intègrent d'autres techniques utilisées en model-checking comme les techniques d'accélérations.</P><p><P align="justify">Suivant une méthodologie rigoureuse, nous instancions ensuite notre algorithme pour une variété de modèles allant des systèmes de transitions finis aux systèmes de transitions infinis. Pour chacun des modèles nous établissons la terminaison de l'algorithme instancié et donnons des résultats expérimentaux préliminaires encourageants.</P><p><p> / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Dans cette thèse, nous considérons deux problèmes auxquels le model checking statistique doit faire face. Le premier concerne les systèmes hétérogènes qui introduisent complexité et non-déterminisme dans l'analyse. Le second problème est celui des propriétés rares, difficiles à observer et donc à quantifier. Pour le premier point, nous présentons des contributions originales pour le formalisme des systèmes composites dans le langage BIP. Nous en proposons une extension stochastique, SBIP, qui permet le recours à l'abstraction stochastique de composants et d'éliminer le non-déterminisme. Ce double effet a pour avantage de réduire la taille du système initial en le remplaçant par un système dont la sémantique est purement stochastique sur lequel les algorithmes de model checking statistique sont définis. La deuxième partie de cette thèse est consacrée à la vérification de propriétés rares. Nous avons proposé le recours à un algorithme original d'échantillonnage préférentiel pour les modèles dont le comportement est décrit à travers un ensemble de commandes. Nous avons également introduit les méthodes multi-niveaux pour la vérification de propriétés rares et nous avons justifié et mis en place l'utilisation d'un algorithme multi-niveau optimal. Ces deux méthodes poursuivent le même objectif de réduire la variance de l'estimateur et le nombre de simulations. Néanmoins, elles sont fondamentalement différentes, la première attaquant le problème au travers du modèle et la seconde au travers des propriétés. / In this thesis, we consider two problems that statistical model checking must cope. The first problem concerns heterogeneous systems, that naturally introduce complexity and non-determinism into the analysis. The second problem concerns rare properties, difficult to observe, and so to quantify. About the first point, we present original contributions for the formalism of composite systems in BIP language. We propose SBIP, a stochastic extension and define its semantics. SBIP allows the recourse to the stochastic abstraction of components and eliminate the non-determinism. This double effect has the advantage of reducing the size of the initial system by replacing it by a system whose semantics is purely stochastic, a necessary requirement for standard statistical model checking algorithms to be applicable. The second part of this thesis is devoted to the verification of rare properties in statistical model checking. We present a state-of-the-art algorithm for models described by a set of guarded commands. Lastly, we motivate the use of importance splitting for statistical model checking and set up an optimal splitting algorithm. Both methods pursue a common goal to reduce the variance of the estimator and the number of simulations. Nevertheless, they are fundamentally different, the first tackling the problem through the model and the second through the properties.

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.

Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with some additional pointers. This is exploited by some currently intensively studied techniques of formal verification that represent an infinite number of states using a finite tree automaton. However, currently there is no tree automata library implementation that would provide an efficient and flexible support for such methods. Thus the aim of this Mas- ter's Thesis is to provide such a library. The present paper first describes the theoretical background of finite tree automata and regular tree languages. Then it surveys the cur- rent implementations of tree automata libraries and studies various verification techniques, outlining requirements for the library. Representation of a finite tree automaton and algo- rithms that perform standard language operations on this representation are proposed in the next part, which is followed by description of library implementation. Through a series of experiments it is shown that the library can compete with other available tree automata libraries, in certain areas being even significantly superior to them.

Probabilistic model checking mainly concentrates on techniques for reasoning about the probabilities of certain path properties or expected values of certain random variables. For the quantitative system analysis, however, there is also another type of interesting performance measure, namely quantiles. A typical quantile query takes as input a lower probability bound p ∈ ]0,1] and a reachability property. The task is then to compute the minimal reward bound r such that with probability at least p the target set will be reached before the accumulated reward exceeds r. Quantiles are well-known from mathematical statistics, but to the best of our knowledge they have not been addressed by the model checking community so far. In this paper, we study the complexity of quantile queries for until properties in discrete-time finite-state Markov decision processes with nonnegative rewards on states. We show that qualitative quantile queries can be evaluated in polynomial time and present an exponential algorithm for the evaluation of quantitative quantile queries. For the special case of Markov chains, we show that quantitative quantile queries can be evaluated in pseudo-polynomial time.

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.

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.