Yes / Model checking has been extensively used to verify various systems. However, this usually has been done by experts who have a good understanding of model checking and who are familiar with the syntax of both modelling and property specification languages. Unfortunately, this is not an easy task for nonexperts to learn description languages for modelling and formal logics/languages for property specification. In particular, property specification is very daunting and error-prone for nonexperts. In this paper, we present a methodology to facilitate probabilistic model checking for nonexperts. The methodology helps nonexpert users model their systems and express their requirements without any knowledge of the modelling and property specification languages.

In this thesis we propose general and simple methods for automatic verification of parameterized systems. These are systems consisting of an arbitrary number of identical processes or components. The number of processes defines the size of the system. A parameterized system may be regarded as an infinite family of instances, namely one for each size. The aim is to perform a parameterized verification, i.e. to verify that behaviors produced by all instances, regardless of their size, comply with some safety or liveness property. In this work, we describe three approaches to parameterized verification. First, we extend the Regular Model Checking framework to systems where components are organized in tree-like structures. For such systems, we give a methodology for computing the set of reachable configurations (used to verify safety properties) and the transitive closure (used to verify liveness properties). Next, we introduce a methodology allowing the verification of safety properties for a large class of parameterized systems. We focus on systems where components are organized in linear arrays and manipulate variables or arrays of variables ranging over bounded or numerical domains. We perform backwards reachability analysis on a uniform over-approximation of the parameterized system at hand. Finally, we suggest a new approach that enables us to reduce the verification of termination under weak fairness conditions to a reachability analysis for systems with simple commutativity properties. The idea is that reachability calculations (associated with safety) are usually less expensive then termination (associated with liveness). This idea can also be used for other transition systems and not only those induced by parameterized systems.

La vérification de propriétés de sûreté des logiciels distribués basés sur des canaux fifo non bornés et fiables mène directement au model checking de systèmes infinis. Nous introduisons la famille des (q)ueueing (c)oncurrent (p)rocesses (QCP) composant des systèmes de transitions locaux, par exemple des automates finis/à pile, qui communiquent entre eux par des files fifo. Le problème d'atteignabilité des états de contrôle est indécidable pour des automates communicants et des automates à plusieurs piles, et par conséquent pour QCP.Nous présentons deux solutions pour contourner ce résultat négatif :Primo, une sur-approximation basée sur l'approche abstraire-tester-raffiner qui s'appuie sur notre nouveau concept de raffinement par chemin. Cette approche mène à permettre d'écrire un semi-algorithme du type CEGAR qui est implémenté avec des QDD et réalisé dans le framework McScM dont le banc d'essai conclut notre présentation.Secundo, nous proposons des restrictions pour les QCP à des piles locales pour démêler l'interaction causale entre les données locales (la pile), et la synchronisation globale. Nous montrons qu'en supposant qu'il existe une borne existentielle sur les exécutions et qu'en ajoutant une condition sur l'architecture, qui entrave la synchronisation de deux piles, on arrive à une réponse positive pour le problème de décidabilité de l'atteignabilité qui est EXPTime-complet (et qui généralise des résultats déjà connus). La construction de base repose sur une simulation du système par un automate à une pile équivalent du point de vue de l'atteignabilité --- sous-jacente, nos deux restrictions restreignent les exécutions à une forme hors-contexte. Nous montrons aussi que ces contraintes apparaissent souvent dans des situations ``concrètes''et qu'elles sont moins restrictives que celles actuellement connues. Une autre possibilité pour arriver à une solution pratiquement utilisable consiste à supposer une borne du problème de décidabilité : nous montrons que l'atteignabilité par un nombre borné de phases est décidable par un algorithme constructif qui est 2EXPTime-complet.Finalement, nous montrons qu'élargir les résultats positifs ci-dessus à la vérification de la logique linéaire temporelle demande soit de sacrifier l'expressivité de la logique soit d'ajouter des restrictions assez fortes aux QCP --- deux restrictions qui rendent cette approche inutilisable en pratique. En réutilisant notre argument de type ``hors-contexte'', nous représentons l'ordre partiel sous-jacent aux exécutions par des grammaires hypergraphes. Cela nous permet de bénéficier de résultats connus concertant le model checking des formules de la logique MSO sur les graphes (avec largeur arborescente bornée), et d'arriver aux premiers résultats concernant la vérification des propriétés sur l'ordre partiel des automates (à pile) communicants. / The safety verification of distributed programs, that are based on reliable, unbounded fifo communication, leads in a straight line to model checking of infinite state systems. We introduce the family of (q)ueueing (c)oncurrent (p)rocesses (QCP): local transition systems, e.g., (pushdown-)automata, that are globally communicating over fifo channels. QCP inherits thus the known negative answers to the control-state reachability question from its members, above all from communicating automata and multi-stack pushdown systems. A feasible resolution of this question is, however, the corner stone for safety verification.We present two solutions to this intricacy: first, an over-approximation in the form of an abstract-check-refine algorithm on top of our novel notion of path invariant based refinement. This leads to a \cegar semi-algorithm that is implemented with the help of QDD and realized in a small software framework (McScM); the latter is benchmarked on a series ofsmall example protocols. Second, we propose restrictions for QCP with local pushdowns that untangle the causal interaction of local data, i.e., thestack, and global synchronization. We prove that an existential boundedness condition on runs together with an architectural restriction, that impedes the synchronization of two pushdowns, is sufficient and leads to an EXPTime-complete decision procedure (thus subsuming and generalizing known results). The underlying construction relies on a control-state reachability equivalent simulation on a single pushdown automaton, i.e., the context-freeness of the runs under the previous restrictions. We can demonstrate that our constraints arise ``naturally'' in certain classes of practical situations and are less restrictive than currently known ones. Another possibility to gain a practicable solution to safety verification involves limiting the decision question itself: we show that bounded phase reachability is decidable by a constructive algorithms in 2ExpTime, which is complete.Finally, trying to directly extend the previous positive results to model checking of linear temporal logic is not possible withouteither sacrificing expressivity or adding strong restrictions (i.e., that are not usable in practice). However, we can lift our context-freeness argument via hyperedge replacement grammars to graph-like representation of the partial order underlying each run of a QCP. Thus, we can directly apply the well-known results on MSO model checking on graphs (of bounded treewidth) to our setting and derive first results on verifying partial order properties on communicating (pushdown-) automata.

Företag inom fordonsindustrin sätter mer och mer press på snabba utvecklingsprocesser och ny avancerad teknik, vilket resulterar i att mindre tid allokeras åt utveckling som kräver mer och mer tid. Syftet med detta examensarbete var att ta fram, utveckla och utvärdera ett automatiskt verifieringssystem lämpat för ett företag inom fordonsindustrin med VT System som testmiljö och Jenkins som byggserver. Utifrån syftet definierades tre frågeställningar som besvarades genom att först undersöka vilka komponenter ett automatiskt verifieringssystem kan innehålla, för att sedan utveckla ett automatiskt verifieringssystem samt en tillhörande arkitektur. Slutligen utvärderades det automatiska verifieringssystemet genom ett experiment för att undersöka dess tidseffektivitet. För att uppnå detta syfte samt besvara examensarbetets frågeställningar valdes Design Science Research som metod för arbetet. Resultatet från experimentet visar på att det inte finns någon signifikant tidseffektivitetsskillnad mellan ett automatiskt verifieringssystem och ett manuellt utförande av samma uppgift. Examensarbetet belyser andra aspekter som det automatiska verifieringssystemet istället kan bidra med till verksamheten. Resultaten från arbetet bidrar till kunskapsområdena automatiska tester och helt autonoma system, detta genom att dels presentera en arkitektur för ett automatiskt verifieringssystem och dels genom resultat från tidigare nämnt experiment. / Automotive companies are increasingly investing in fast development processes and new advanced technology, resulting in less time being allocated to development that is more time consuming. The purpose of this thesis was to develop and evaluate an automatic verification system adapted for companies within the automotive industry with VT System as test environment and Jenkins as build server. Based on this purpose, three research questions were defined and then answered by first investigating which components an automatic verification system could contain. This was followed by the development of an automatic verification system and a corresponding architecture. Finally, the automatic verification system was evaluated through an experiment, with the purpose of investigating it’s time efficiency. To achieve the purpose of this thesis the method Design Science Research was used. The results from the experiment shows that there is no significant difference in time efficiency between the automatic verification system and a manual approach of the same task. The thesis highlights other aspects of the automatic verification system in which it can contribute. The result of the work contributes to different knowledge areas such as automated testing and fully automated systems, it does this by presenting an architecture for an automatic verification system and by presenting the result from the above-mentioned experiment.

ROS2 is an increasingly popular middleware framework for developing robotic applications. A ROS2 applicationbasically is composed of nodes that run concurrently and can be deployed distributedly. ROS2 nodes communicatewith each other through asynchronous interfaces; they reside in memory and wait to respond events that circulatearound the system during the interactions between the robot(s) and the environment. Rebeca is an actor-basedlanguage for modelling asynchronous, concurrent applications. Timed Rebeca added timing features to Rebeca todeal with timing requirements of real-time systems. The similarities in the concurrency and message-basedasynchronous interactions ofreactive nodes justify the relevance of using Timed Rebeca to assist the developmentand verification of ROS2 applications. Model-based development and model checking allow quicker prototypingand earlier detection ofsystem errors without the requirement of developing the entire real system. However, thereare challenges in bridging the gaps between continuous behaviours in a real robotic system and discrete behavioursin a model, between complex computations in a robotic system and the inequivalent programming facilities in amodelling language. There have been previous attempts in mapping Rebeca to ROS, however they could not beput into practice due to over-simplifications or improper modelling approaches. This thesis addresses the problemfrom a more systematic perspective and has been successful in modelling a realistic multiple autonomous mobilerobots system, creating corresponding ROS2 demonstration code, showing the synchronization between the modeland the program to prove the values of the model in driving development and automatic verification of correctnessproperties (freedom ofdeadlocks, collisions, and congestions). Stability of model checking results confirms designproblems that are not always detected by simulation. The modelling principles, modelling and implementingtechniques that are invented and summarized in this work can be reused for many other cases.

CoordenaÃÃo de AperfeiÃoamento de Pessoal de NÃvel Superior / As Linhas de produtos de software sÃo uma forma de maximizar o reuso de software, dado que proveem a customizaÃÃo de software em massa. Recentemente, Linhas de produtos de software (LPSs) tÃm sido usadas para oferecer suporte ao desenvolvimento de aplicaÃÃes sensÃveis ao contexto nas quais adaptabilidade em tempo de execuÃÃo à um requisito importante. Neste caso, as LPSs sÃo denominadas Linhas de produtos de software sensÃveis ao contexto (LPSSCs). O sucesso de uma LPSSC depende, portanto, da modelagem de suas caracterÃsticas e do contexto que lhe à relevante. Neste trabalho, essa modelagem à feita usando o diagrama de caracterÃsticas e o diagrama de contexto. Entretanto, um processo manual para construÃÃo e configuraÃÃo desses modelos pode facilitar a inclusÃo de diversos erros, tais como duplicaÃÃo de caracterÃsticas, ciclos, caracterÃsticas mortas e falsos opcionais sendo, portanto, necessÃrio o uso de tÃcnicas de verificaÃÃo de consistÃncia. A verificaÃÃo de consistÃncia neste domÃnio de aplicaÃÃes assume um papel importante, pois as aplicaÃÃes usam contexto tanto para prover serviÃos como para auto-adaptaÃÃo caso seja necessÃrio. Neste sentido, as adaptaÃÃes disparadas por mudanÃas de contexto podem levar a aplicaÃÃo a um estado indesejado. AlÃm disso, a descoberta de que algumas adaptaÃÃes podem levar a estados indesejados sà pode ser atestada durante a execuÃÃo pois o erro à condicionado à configuraÃÃo atual do produto. Ao considerar que tais aplicaÃÃes estÃo sujeitas a um grande volume de mudanÃas contextuais, a verificaÃÃo manual torna-se impraticÃvel. Logo, à interessante que seja possÃvel realizar a verificaÃÃo da consistÃncia de forma automatizada de maneira que uma entidade computacional possa realizar essas operaÃÃes. Dado o pouco suporte automatizado oferecido a esses processos, o objetivo deste trabalho à propor a automatizaÃÃo completa desses processos com uma ferramenta, chamada FixTure (FixTure), para realizar a verificaÃÃo da construÃÃo dos modelos de caracterÃsticas para LPSSC e da configuraÃÃo de produtos a partir desses modelos. A ferramenta FixTure tambÃm provà uma simulaÃÃo de situaÃÃes de contexto no ciclo de vida de uma aplicaÃÃo de uma LPSSC, com o objetivo de identificar inconsistÃncias que ocorreriam em tempo de execuÃÃo. / Software product lines are a way to maximize software reuse once it provides mass software customization. Software product lines (SPLs) have been also used to support contextaware applicationâs development where adaptability at runtime is an important issue. In this case, SPLs are known as Context-aware software product lines. Context-aware software product line (CASPL) success depends on the modelling of their features and relevant context. However, a manual process to build and configure these models can add several errors such as replicated features, loops, and dead and false optional features. Because of this, there is a need of techniques to verify the model consistency. In the context-aware application domain, the consistency verification plays an important role, since application in this domain use context to both provide services and self-adaptation, when it is needed. In this sense, context-triggered adaptations may lead the application to undesired state. Moreover, in some cases, the statement that a contex-triggered adaptation is undesired only can be made at runtime, because the error is conditioned to the current product configuration. Additionally, applications in this domain are submitted to large volumes of contextual changes, which imply that manual verification is virtually not viable. So, it is interesting to do consistency verification in a automated way such that a computational entity may execute these operations. As there is few automated support for these proccesses, the objective of this work is to propose the complete automation of these proccesses with a software tool, called FixTure, that does consistency verification of feature diagrams during their development and product configuration. FixTure tool also supports contextual changes simulation during the lifecycle of a CASPL application in order to identify inconsistencies that can happen at runtime.