Programmed Cell Death, or Apoptosis, plays a critical role in human embryonic development and in adult tissue homeostasis. Recent research efforts in Bioinformatics and Computational Biology focus on gaining deep insight into the Apoptosis process. This allows researchers to clearly study the relation between the dysregulation of apoptosis and the development of cancer. Research in this highly interdisciplinary field of bioinformatics has become much more quantitative, using tools from computational sciences to understand the behavior of Biological systems. Previously, an abstracted model has been developed to study the Apoptosis process as a Finite State Discrete Transition Model. This model facilitates the reutilization of the digital design verification and testing techniques developed in the Electronic Design Automation domain. These verification and testing techniques for hardware have become robust over the past few decades. Usually simulation is the cornerstone of the Design Verification industry and bulk of states are covered by simulation. Formal verification techniques are then used to analyze the remaining corner case states. Techniques like Genetic Algorithm guided Logic Simulation (GALS) and SAT-based Induction have already been applied to the Apoptosis Discrete Transition Model. However, the Apoptosis model presents some unique problems. The simulation techniques have shown to be unable to cover most of the states of the Apoptosis model. When SAT-based Induction is applied to the Apoptosis model, in particular to find illegal states, very few illegal states are identified. It particularly suffers from the fact that the Apoptosis Model is rather complex and the formulation for testing and verification is hard to tackle at larger bounds greater than 20 or so. Consequently, the state space of the Apoptosis model largely lies in the unknown region, meaning that we are unable to either reach those states or prove that they are illegal. Unless we know whether these states are reachable or illegal, it is not feasible to infer information about the model such as what protein concentrations can be reached under what kind of input stimuli. Questions such as whether certain protein concentrations can be reached or not in this model can only be answered if we have a clear picture of the reachability of state space. In this thesis, we propose techniques based on ATPG and SAT based image computation of the Apoptosis finite transition model. Our method leverages the results obtained in previous research work. It uses the reachable states obtained from the simulation traces of the previous work as initial states for our technique. This enables us to identify more illegal states in less number of iterations; in other words, we are able to reach the fixed point in image computation faster. Our experimental analysis illustrates that the proposed techniques could prove most of the former unknown states as illegal states. We are able to extend our analysis to obtain clearer picture of the interaction of any two proteins in the system considered together. / Master of Science

Devido à alta complexidade dos Sistemas Produtivos, o projeto de sistemas de controle adequados às exigências normativas vinculadas aos processos industriais que são executados, e seu impacto no ser humano e no ambiente demandam a necessidade do desenvolvimento de soluções de controle que sejam seguras e estáveis no sentido de não causar interrupções no processo produtivo e danos ao ser humano e ao meio. Uma abordagem para o desenvolvimento de sistemas que contemplem estes requisitos baseia-se no conceito de Sistemas Instrumentados de Segurança e na aplicação das normas IEC 61508 e IEC 61511. Entretanto, assim como o desenvolvimento de qualquer software, os programas de controle de SIS também estão sujeitos a erros de especificação e projeto, mesmo quando o desenvolvimento é feito conforme os critérios normatizados. Além dos erros de projeto, também deve ser levado em consideração que as camadas de prevenção e mitigação especificadas nas normas podem ser desenvolvidas separadamente e dessa forma podem ocorrer comportamentos não previstos ou indesejáveis quando da operação conjunta delas. Uma das formas para uma melhoria na confiabilidade desses programas e que também é um requerimento pertinente ao ciclo de desenvolvimento de um SIS - de acordo com as normas de segurança IEC 61508 e IEC 61511 - é a aplicação de técnicas de verificação formal dos modelos desses programas de controle bem como o uso de um ambiente unificado para modelagem desses sistemas de controle, onde suas interações possam ser mais bem compreendidas. Atualmente, umas das técnicas mais proeminentes para a verificação de sistemas é o Model Checking, que realiza uma busca exaustiva no espaço de estados de um sistema dirigido por eventos, verificando as propriedades especificadas a partir de proposições estabelecidas em lógica temporal. Para esse trabalho é utilizada a lógica TCTL devido a sua capacidade de expressar propriedades em domínio temporal denso. Como ferramenta computacional será usado o ambiente GHENeSys, que propicia um ambiente unificado para modelagem, simulação e verificação dos sistemas por conjugar os benefícios de rede de Petri para modelagem e as técnicas de Model Checking para verificação de modelos. / Due to the high complexity of the actual Productive Systems, the design of suitable control systems according to the applicable industrial standards, and the possible negative impacts on the human being, on the environment and on equipment, the development of control solutions that are be both secure and stable as some systems have to operate nonstop is much demanded. One approach for the development systems with such requirements is the use of Safety Instrumented Systems complying with the standards IEC 61508 and IEC 61511. However, as on the development of any kind of software, SIS control programs are also prone to specification and design errors, even when the control programs are developed according to the applicable standards. Besides design errors, must be taken into consideration the fact that the SIS prevention and mitigation layers, as prescribed on the standards, can be developed individually and thus presenting unanticipated or undesirable behaviors when operating together. One way to improve the reliability of these control programs, which is also required by the safety standards IEC 61508 and IEC 61511 as part of the SIS development cycle, is the application of formal verification techniques on the control software models. Another way is to use a unified approach for modeling these control systems, and thus having the opportunity to understand their interactions better. Currently, one of the most prominent techniques for the verification of systems is the Model Checking. Such technique performs an exhaustive search in the space state of an event driven system, verifying the properties specified as established propositions in temporal logic. On this work, the TCTL logic is used due its ability to express properties in the dense time domain. As computational tool will be used GHENeSys environment, as it provides a unified environment for modeling, simulating and the verification of systems, which enjoys the benefits of modelling through Petri Nets and Model Checking techniques for formal verification.

Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA. / Software-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA.

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles. / The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks.

Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.

Les travaux décrits dans cette thèse portent sur le problème de vérification des systèmes avec espaces d’états infinis, et, en particulier, avec des structures de données chaînées. Plusieurs approches ont émergé, sans donner des solutions convenables et robustes, qui pourrait faire face aux situations rencontrées dans la pratique. Nos travaux proposent une approche nouvelle, qui combine les avantages de deux approches très prometteuses: la représentation symbolique a base d’automates d’arbre, et la logique de séparation. On présente également plusieurs améliorations concernant l’implementation de différentes opérations sur les automates d’arbre, requises pour le succès pratique de notre méthode. En particulier, on propose un algorithme optimise pour le calcul des simulations sur les systèmes de transitions étiquettes, qui se traduit dans un algorithme efficace pour le calcul des simulations sur les automates d’arbre. En outre, on présente un nouvel algorithme pour le problème d’inclusion sur les automates d’arbre. Un nombre important d’expérimentes montre que cet algorithme est plus efficace que certaines des méthodes existantes. / This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating that the new algorithm outperforms other existing approaches.

Devido à alta complexidade dos Sistemas Produtivos, o projeto de sistemas de controle adequados às exigências normativas vinculadas aos processos industriais que são executados, e seu impacto no ser humano e no ambiente demandam a necessidade do desenvolvimento de soluções de controle que sejam seguras e estáveis no sentido de não causar interrupções no processo produtivo e danos ao ser humano e ao meio. Uma abordagem para o desenvolvimento de sistemas que contemplem estes requisitos baseia-se no conceito de Sistemas Instrumentados de Segurança e na aplicação das normas IEC 61508 e IEC 61511. Entretanto, assim como o desenvolvimento de qualquer software, os programas de controle de SIS também estão sujeitos a erros de especificação e projeto, mesmo quando o desenvolvimento é feito conforme os critérios normatizados. Além dos erros de projeto, também deve ser levado em consideração que as camadas de prevenção e mitigação especificadas nas normas podem ser desenvolvidas separadamente e dessa forma podem ocorrer comportamentos não previstos ou indesejáveis quando da operação conjunta delas. Uma das formas para uma melhoria na confiabilidade desses programas e que também é um requerimento pertinente ao ciclo de desenvolvimento de um SIS - de acordo com as normas de segurança IEC 61508 e IEC 61511 - é a aplicação de técnicas de verificação formal dos modelos desses programas de controle bem como o uso de um ambiente unificado para modelagem desses sistemas de controle, onde suas interações possam ser mais bem compreendidas. Atualmente, umas das técnicas mais proeminentes para a verificação de sistemas é o Model Checking, que realiza uma busca exaustiva no espaço de estados de um sistema dirigido por eventos, verificando as propriedades especificadas a partir de proposições estabelecidas em lógica temporal. Para esse trabalho é utilizada a lógica TCTL devido a sua capacidade de expressar propriedades em domínio temporal denso. Como ferramenta computacional será usado o ambiente GHENeSys, que propicia um ambiente unificado para modelagem, simulação e verificação dos sistemas por conjugar os benefícios de rede de Petri para modelagem e as técnicas de Model Checking para verificação de modelos. / Due to the high complexity of the actual Productive Systems, the design of suitable control systems according to the applicable industrial standards, and the possible negative impacts on the human being, on the environment and on equipment, the development of control solutions that are be both secure and stable as some systems have to operate nonstop is much demanded. One approach for the development systems with such requirements is the use of Safety Instrumented Systems complying with the standards IEC 61508 and IEC 61511. However, as on the development of any kind of software, SIS control programs are also prone to specification and design errors, even when the control programs are developed according to the applicable standards. Besides design errors, must be taken into consideration the fact that the SIS prevention and mitigation layers, as prescribed on the standards, can be developed individually and thus presenting unanticipated or undesirable behaviors when operating together. One way to improve the reliability of these control programs, which is also required by the safety standards IEC 61508 and IEC 61511 as part of the SIS development cycle, is the application of formal verification techniques on the control software models. Another way is to use a unified approach for modeling these control systems, and thus having the opportunity to understand their interactions better. Currently, one of the most prominent techniques for the verification of systems is the Model Checking. Such technique performs an exhaustive search in the space state of an event driven system, verifying the properties specified as established propositions in temporal logic. On this work, the TCTL logic is used due its ability to express properties in the dense time domain. As computational tool will be used GHENeSys environment, as it provides a unified environment for modeling, simulating and the verification of systems, which enjoys the benefits of modelling through Petri Nets and Model Checking techniques for formal verification.

Abstract. Since the introduction of interpolants to the field of symbolic model checking, interpolation-based methods have been successfully used in both hardware and software model checking. Recently, variable assignments have been introduced to the computation of interpolants. In the context of abstract reachability graphs, variable assignment can be used not only to prevent out-of-scope variables from appearing in interpolants, but also to reduce the size of the interpolant significantly. We further extend the framework for computing interpolants under variable assignment, prove the correctness of the system and show that it has potential to further decrease the size of the computed interpolants. At the end we analyze under which conditions the computed interpolants will still have the path interpolation property, a desired property in many interpolation-based techniques. 1

La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées. / Workflow technology, whose role is to automate business processes and to provide a support for their management, is today an active sector of research. This thesis deals with the modelling of the workflow processes and their analysis. These processes, probably constrained by shared resources or by durations of treatment, must be checked before being executed by their workflow management systems. In this direction, we were interested by the checking of the soundness property of workflow nets (WF-nets): subclasses of Petri nets modelling the workflow processes.To begin with, by exploring the structure theory of Petri nets, we have identified subclasses of WF-nets for which soundness can be checked and characterized effectively. We also extended these subclasses by taking account of the presence of shared resources and we focused on the soundness property in the presence of an arbitrary number of instances ready to be carried out. In this part, we had to automate the computation of minimal siphons in a Petri net. For that, we chose an algorithm of the literature and improved it by the research and the contraction of alternate circuits.Then, we were concerned by the modelling and the analysis of workflow processes holding temporal constraints. We initially proposed the model of TWF-net (Timed WF-net). For this model, we defined its soundness and proposed a method to check it. Then, we released the adopted temporal constraints by the proposal of a model covering workflow processes for witch temporal constraints vary in time intervals. We formally defined the model of ITWF-net (Interval Timed WF-net) and gave its semantics. In addition, we developed and tested a prototype of modelling and simulation of ITWF-nets.The last part of this thesis concerns the formal analysis of workflow processes with SPIN model checker. We initially translated the workflow specification into Promela: the model description language used by SPIN. Then, we expressed the soundness properties in Linear Temporal Logic (LTL) and used SPIN to test if each property is satisfied by the Promela model of a given WF-net. Moreover, we expressed the properties of k-soundness for WF-nets modelling several instances and (k,R)-soundness for competitive workflow processes which share resources.

Model checking is a powerful technique for analyzing reach ability and temporal properties of finite state systems. Model-checking finite state systems has been well-studied and there are well known efficient algorithms for this problem. However these algorithms may not terminate when applied directly to in finite state systems. Counter systems are a class of in fininite state systems where the domain of counter values is possibly in finite. Many practical systems like cache coherence protocols, broadcast protocols etc, can naturally be modeled as counter systems. In this thesis we identify a class of counter systems, and propose a new technique to check whether a system from this class satires’ a given CTL formula. The key novelty of our approach is a way to use existing reach ability analysis techniques to answer both \until" and \global" properties; also our technique for \global" properties is different from previous techniques that work on other classes of counter systems, as well as other classes of in finite state systems. We also provide some results by applying our approach to several natural examples, which illustrates the scope of our approach.