The ultimate goal of SPIN and indeed of all testing or validation methodology is to demonstrate, with a certain degree of confidence, that a proposed design or implementation meets its requirements. SPIN is a tool to simulate and validate Protocols. Promela, its source language, is a formal description technique like SDL and Estelle that is based on communicating state atomata. Unlike most other tools, SPIN is in the public domain and therefore is one of the most widely used formal verification tools today. Paper presents a formalization method of piece linear aggregates (PLA) and an investigation of possibilities to use SPIN system for validation of PLA specifications of distributed systems. It is shown that in order to write Promela specifications, processes used in the PLA model should be represented by finite state automata. PLA specification of two protocols, its description by finite state automata and its verification results in SPIN system are presented. It is shown in this paper that the SPIN system can be used for the verification of aggregate specifications. Using the SPIN system the finite state graphs of the processes used in the formal specification have to be formed. Then they have to be described in the Promela language.

Master of Science / Department of Computing and Information Sciences / Gurdip Singh / PROMELA stands for Protocol Meta Language. It is a modeling language for developing distributed systems. It allows for the dynamic creation of concurrent processes which can communicate through message channels. DAJ stands for Distributed Algorithms in Java. It is a Java toolkit for designing, implementing, simulating, and visualizing distributed algorithms. The toolkit consists of Java class library with a simple programming interface that allows development of distributed algorithms based on a message passing model. It also provides a visualization environment where the protocol execution can be paused, performed step by step, and restarted. This project is a Java application designed to translate a model written in Promela into a model using the Java class library provided by DAJ and simulate it using DAJ. Even though there are similarities between the programming constructs of Promela and DAJ, the programming interface supported by DAJ is smaller, so the input has been confined to a variant, which is a subset of Promela. The implementation was performed in three steps. In the first step an input domain was defined and an ANTLR grammar was defined for the input structure. Java code has been embedded to this ANTLR grammar so that it can parse the input and translates it into an intermediate xml format. In the second step, a String Template is used which would consist of templates of the output model, along with a Java program which traverses the intermediate xml file and generates the output model. In the third step, the obtained output model is compiled and then simulated and visualized using DAJ. The application has been tested over input models having different topologies, process nodes, messages, and variables and covering most of the input domain.

De nos jours, la mise au point de logiciels ou de systèmes fiables est de plus en plus difficile. Les nouvelles technologies impliquent de plus en plus d'interactions entre composants complexes, dont l'analyse et la compréhension deviennent de plus en plus délicates. Pour pallier ce problème, les domaines de la vérification et de la validation ont connu un bond significatif avec la mise au point de nouvelles méthodes, réparties en deux grandes familles : la vérification formelle et la simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. Dans ce cadre, les travaux de cette thèse proposent une nouvelle approche pour intégrer la simulation dites à évènements discrets aux méthodes formelles. L'objectif est d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter des erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux. / Nowadays, making reliable software and systems is become harder. New technologies imply more and more interactions between complex components, whose the analysis and the understanding are become arduous.To overcome this problem, the domains of verification and validation have known a significant progress, with the emergence of new automatic methods that ensure reliability of systems. Among all these techniques, we can find two great families of tools : the formal methods and the simulation. For a long time, these two families have been considered as opposite to each other. However, recent work tries to reduce the border between them. In this context, this thesis proposes a new approach in order to integrate discrete-event simulation in formal methods. The main objective is to improve existing model-checking tools by combining them with simulation, in order to allow them detecting errors that they were not previously able to find, and especially on timed systems. This approach led us to develop a new formal language, called DEv-PROMELA. This new language, which relies on the PROMELA and on the DEVS formalism, is like both a verifiable specifications language and a simulation formalism. By combining a traditional model-checking and a discrete-event simulation on models expressed in DEv-PROMELA, it is therefore possible to detect and to understand dysfunctions which could not be found by using only a formal checking or only a simulation. This result is illustrated through the different examples which are treated in this work.

Företag förlitar sig ofta på datalager som aggregerar information från flera källor och över tiden. Dessa datalager är ofta centrala för beslutsfattande inom företagen, både kortsiktiga operativa beslut och långsiktiga strategiska. Eftersom information är en färskvara blir det allt viktigare att de dagliga laddningsrutinerna för datalagren fungerar. Denna rapport avser att analysera möjligheten att applicera principen model checking för en validering. Praktiskt avses att på ett automatiserat sätt använda Promela och Spin som verktyg för att validera att laddningsrutinerna för datalagret är korrekta. / Companies of today put more and more trust into data warehouses that aggregates information from several sources and over time. These data warehouses are pivotal for decision making both for daily operational decisions and for long term strategic ones. Since information is a perishable it has become more and more important that the loading routines for the data warehouses works. This essay will look into the possibility to automatically transform the load procedures to use Promela and Spin as tools to validate that the data warehouse load.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

M. Tech. Electrical Engineering. / This research presented an integrated formal model of the JXTA protocol suite. The integrated model is constructed from the individual models describing the behaviours of protocols entities. Written in the PROMELA specification language, the finite state automata of these models are shown instead. The SPIN-based formal verification revealed that this studys integrated model was too large to perform for the computational resources available. This was in spite of the application of multiple complexity reduction techniques. Subsequently, as final recourse, the research resorted to the formal verification of individual protocols by making further abstraction of the interaction and dependencies between protocols. A number of errors were found including an invalid end state in the routing protocols and multiple non-progress cycles.

Vérification Formelle et Incrémentale de Spécifications SysML pour la Conception de Systèmes à Base de ComposantsLe travail présenté dans cette thèse est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisé avec le langage SysML. Les SBC sont largement utilisés dans le domaine industrielet ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l'utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en {\oe}uvre d'approches plus rigoureuses.Pour faciliter la communication entre les différentes parties impliquées dans le développement d'un SBC, un des langages largement utilisé est SysML, qui permet de modéliser, en plus de la structure et le comportement du système, aussi ses exigences. Il offre un standard de modélisation, spécification et documentation de systèmes, dans lequel il est possible de développer un système, partant d'un niveau abstrait, vers des niveaux plus détaillés pouvant aboutir à une implémentation. %Généralement ces systèmes sont faits plus grands parce qu'ils sont développés avec des cadres logiciels.Dans ce contexte nous avons traité principalement deux problématiques.La première est liée au développement par raffinement d'un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu'une composition d'un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d'un SBC. Dans cette contribution, nous exploitons les outils: Ptolemy pour la vérification de la compatibilité des composants assemblés, et l'outil MIO Workbench pour la vérification du raffinementLa deuxième problématique traitée concerne la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante: comment spécifier une architecture SBC qui satisfait toutes les exigences du système? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d'interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le model-checker SPIN et la LTL pour spécifier et vérifier les exigences.Mots clés: {Modélisation, Spécifications SysML, Architecture SBC, Raffinement, Compatibilité, Exigences, Propriétés LTL, Promela/SPIN, Ptolemy, MIO Workbench} / Formal and Incremental Verification of SysML Specifications for the Design of Component-Based SystemsThe work presented in this thesis is a contribution to the specification and verification of Component-Based Systems (CBS) modeled in SysML. CBS are widely used on the industrial field, and they are built by assembling various reusable components, allowing developing complex systems at lower cost.Despite the success of the use of CBS, their design is an increasingly complex step that requires the implementation of more rigorous approaches.To ease the communication between the various stakeholders in a CBS development project, one of the widely used modeling languages is SysML, which besides allowing modeling of structure and behavior, it has capabilities to model requirements. It offers a standard for modeling, specifying and documenting systems, wherein it is possible to develop a system, starting from an abstract level, to more detailed levels that may lead to an implementation.In this context, we have dealt mainly two issues. The first one concerns the development by refinement of a CBS, which is described only by its SysML interfaces and behavior protocols. Our contribution allows the designer of CBS to formally ensure that a composition of a set of elementary and reusable components refines an abstract specification of a CBS. In this contribution, we use the tools: Ptolemy for the verification of compatibility of the assembled components and MIO Workbench for refinement verification.The second one concerns the difficulty to decide what to build and how to build it, considering only system requirements and reusable components. Therefore, the question that arises is: how to specify a CBS architecture, which satisfies all system requirements? We propose a formal and incremental verification approach based on SysML models and interface automata to guide, by the requirements, the CBS designer to define a coherent system architecture that satisfies all proposed SysML requirements. In this approach we use the SPIN model-checker and LTL properties to specify and verify requirements.Keywords: {Modeling, SysML specifications, CBS architecture, Refinement, Compatibility, Requirements, LTL properties, Promela/SPIN, Ptolemy, MIO Workbench}

One problem with computers is that the operating system automatically trusts any externallyconnected peripheral. This can result in abuse when a peripheral technically can violate the security model because the peripheral is trusted. Because of that the security is an important issue to look at.The aim of our project is to see in which cases hardware peripherals can be trusted. We built amodel of the universal asynchronous transmitter/receiver (UART), a model of the main memory(RAM) and a model of a DMA controller. We analysed interaction between hardware peripherals,user processes and the main memory.One of our results is that connections with hardware peripherals are secure if the hardware is properly configured. A threat scenario could be an eavesdropper or man-in-the-middle trying to steal data or change a cryptographic key.We consider the use-cases of DMA and protecting a cryptographic key. We prove the well-behavior of the algorithm. Some error-traces resulted from incorrect modelling that was resolved by adjusting the models. Benchmarks were done for different memory sizes.The result is that a peripheral can be trusted provided a configuration is done. Our models consist of finite state machines and their corresponding SMV modules. The models represent computer hardware with DMA. We verified the SMV models using the model checkers NuSMV and nuXmv. / Målet med vårt projekt är att verifiera olika specifikationer av externa enheter som ansluts till datorn. Vi utför formell verifikation av sådan datorutrustning och virtuellt minne. Verifikation med temporal logik, LTL, utförs. Specifikt verifierar vi 4 olika use-case och 9 formler för seriell datakommunikation, DMA och virtuellt minne. Slutsatsen är att anslutning av extern hårdvara är säker om den är ordentligt konfigurerad.Vi gör jämförelser mellan olika minnesstorlekar och mätte tidsåtgången för att verifiera olika system. Vi ser att tidsåtgången för verifikation är långsammare än linjärt beroende och att relativt små system tar relativt lång tid att verifiera.

De nombreux systèmes hétérogènes sont complexes et critiques. Ces systèmes intègrent du logiciel et des composants matériels avec des interactions fortes entre ces composants. Dans ce contexte, il est devenu absolument nécessaire de développer des méthodologies et des techniques pour spéciier et valider ces systèmes.Dans l'ingénierie des systèmes, les exigences sont l'expression des besoins qu'un produit spécifique ou un service doit réaliser. Elles sont définies formellement à de nombreuses occasions dans l'ingénierie des systèmes complexes. Dans ce type de système, deux catégories d'exigence sont présentes : les exigences non-fonctionnelles telles que la performance et la fiabilité, les exigences fonctionnelles telles que la vivacité. Pour valider ces exigences, un environnement permettant de simuler et vérifier ces propriétés est essentiel.Dans notre travail, nous proposons une méthodologie basée sur SysML et combinée avec SystemC et Promela/SPIN pour spéciier et valider des systèmes complexes. Cette approche est basée sur l'ingénierie dirigée par les modèles pour premièrement traduire des modèles SysML en SystemC afin de réaliser des simulations et deuxièmement traduire des diagrammes d'état SysML en Promela/SPINain de vérifier des propriétés temporelles extraites des exigences. Cette approche est expérimentée sur une étude de cas pour démontrer sa faisabilité. / Heterogeneous Systems are complex and become very critical. These systems integrate software andhardware components with intensive interaction between them. In this context, there is a strongnecessity to develop methodologies and techniques to specify and validate these systems.In engineering, the requirements are the expression of needs on what a particular product or a serviceshould be or to make. They are used most of the time in a formal sense in the systems engineering.In this kind of systems, several types of requirements are present: non-functional requirements suchas the performance and the reliability and functional requirements such as the liveliness. To validatethese requirements of a system, an environment to simulate and to check the properties is essential.In our work, we propose a methodology based on SysML combined with SystemC and Promela/SPINto specify and validate complex systems. This approach is based on Model Driven Engineeringtechniques to irstly translate SysML models to systemC with the aim of simulation and to mapSysML behavioral diagrams to Promela/SPIN in order to verify temporal properties extracted fromthe requirements. The approach is experimented on case studies to demonstrate its feasibility.