The problem of relating inter-agent and intra-agent behavioral specifications is investigated. These two views are complimentary, in that the former is closer to scenario-based user requirements whereas the latter is design-oriented. We use a graphical, user-friendly and very simple language as inter-agent specification language: Live Sequence Charts (LSC). LSC is presented and its properties are investigated: it is highly succinct, but inexpressive. There are essentially two ways to relate inter-agent and intra-agent specifications: (i) by checking that an intra-agent specification is correct with respect to some LSC specification and (ii) by automatically building an intra-agent specification from an LSC specification. Several variants of these problems exist: closed/open systems and centralized/distributed systems. We give inefficient but optimal algorithms solving all problems, besides synthesis of open distributed systems, which we show is undecidable. All the problems considered are difficult, even for a very restricted subset of LSCs, without alternatives, interleaving, conditions nor loops. We investigate the cost of extending the language with control flow constructs, conditions, real-time and symbolic instances. An implementation of the algorithms is proposed. The applicability of the language is illustrated on a real-world case study.

Wireless network access protocols are used in numerous safety critical applications. Network availability is essential for safety critical applications,since loss of availability can cause personal or material damage. An adversary can disrupt the availability of a wireless network using denial of service (DoS) attacks. The most widely used wireless protocols are vulnerable to DoS attacks. Researchers have published DoS attacks against IEEE 802.11 local area networks (LANs), IEEE 802.16 wide area networks (WANs) and GSM andUMTS mobile networks. In this work, we analyze DoS vulnerabilities in wireless network protocols and define four categories of attacks:  jamming attacks, flooding attacks, semantic attacks and implementation specific attacks. We identify semantic attacks as the most severe threat to current andfuture wireless protocols, and as the category that has received the least attention by researchers. During the first phase of the research project we discover semantic DoS vulnerabilities in the IEEE 802.11 communication protocols through manual analysis. The 802.11 standard has been subject to manual analysis of DoS vulnerabilities for more than a decade, thus our results indicate that protocol vulnerabilities can elude manual analysis. We conclude that formal methods are required in order to improve protocol robustness against semantic DoS attacks.We propose a formal method that can be used to automatically discover protocol vulnerabilities. The formal method defines a protocol model, adversary model and cost model. The protocol participants and adversary are modeled as finite state transducers, while the cost is modeled as a function of time. Our primary goal is to construct a formal method that is practical, i.e. does not require a vast amount of resources to implement, and useful, i.e. able to discover protocol vulnerabilities. We verify and validate our proposed method by modeling the 802.11w amendment to the 802.11 standard using Promela as the modeling language. We then use the SPIN model checker to verify the model properties and experiments to validate the results. The modeling and experiments result in the discovery and experimental validation of four new deadlock vulnerabilities that had eluded manual analysis. We find one deadlock vulnerability in 802.11i and three deadlock vulnerabilitiesin 802.11w. A deadlock vulnerability is the most severe form of communication protocol DoS vulnerabilities, and their discovery and removal are an essential part of robust protocol design. Thus, we conclude that our proposed formal method is both practical and useful.

A formal specification language used during the requirements phase can reduce errors and rework, but formal specifications are regarded as expensive to maintain, discouraging their adoption. This work presents a single-subject experiment that explores the costs of modifying specifications written in two different languages: a tabular notation, Software Cost Reduction (SCR), and a state-of-the-practice notation, Real-time Unified Modeling Language (UML). The study records the person-hours required to write each specification, the number of defects made during each specification effort, and the amount of time repairing these defects. Two different problems are specified&mdash;a Bidirectional Formatter (BDF), and a Bicycle Computer (BC)&mdash;to balance a learning effect from specifying the same problem twice with different specification languages. During the experiment, an updated feature for each problem is sent to the subject and each specification is modified to reflect the changes. <br /><br /> The results show that the cost to modify a specification are highly dependent on both the problem and the language used. There is no evidence that a tabular notation is easier to modify than a state-of-the-practice notation. <br /><br /> A side-effect of the experiment indicates there is a strong learning effect, independent of the language: in the BDF problem, the second time specifying the problem required more time, but resulted in a better-quality specification than the first time; in the BC problem, the second time specifying the problem required less time and resulted in the same quality specification as the first time. <br /><br /> This work demonstrates also that single-subject experiments can add important information to the growing body of empirical data about the use of formal requirements specifications in software development.

A formal specification language used during the requirements phase can reduce errors and rework, but formal specifications are regarded as expensive to maintain, discouraging their adoption. This work presents a single-subject experiment that explores the costs of modifying specifications written in two different languages: a tabular notation, Software Cost Reduction (SCR), and a state-of-the-practice notation, Real-time Unified Modeling Language (UML). The study records the person-hours required to write each specification, the number of defects made during each specification effort, and the amount of time repairing these defects. Two different problems are specified&mdash;a Bidirectional Formatter (BDF), and a Bicycle Computer (BC)&mdash;to balance a learning effect from specifying the same problem twice with different specification languages. During the experiment, an updated feature for each problem is sent to the subject and each specification is modified to reflect the changes. <br /><br /> The results show that the cost to modify a specification are highly dependent on both the problem and the language used. There is no evidence that a tabular notation is easier to modify than a state-of-the-practice notation. <br /><br /> A side-effect of the experiment indicates there is a strong learning effect, independent of the language: in the BDF problem, the second time specifying the problem required more time, but resulted in a better-quality specification than the first time; in the BC problem, the second time specifying the problem required less time and resulted in the same quality specification as the first time. <br /><br /> This work demonstrates also that single-subject experiments can add important information to the growing body of empirical data about the use of formal requirements specifications in software development.

Reuse of software designs, experience and components is essential to making substantial improvements in software productivity, development cost, and quality. However, the many facets of reuse are still rarely used in the various phases of the software development lifecycle because of a lack of adequate theories, processes, and tools to support consistent application of reuse concepts. There is a need for approaches including definitions, models and properties of reuse that would provide explicit guidance to a software development team in applying reuse. In particular there is a need to provide abstractions that clearly separate the various functional concerns addressed in a software system. Separating concerns simplifies the identification of the software components that can benefit from reuse and can provide guidance on how reuse may be applied. In this thesis we present an extended model related to the separation of concerns in object-oriented design. The model, called views, indicates how an object-oriented design can be clearly separated into objects and their corresponding interfaces. In this model objects can be designed so that they are independent of their environment, because adaptation to the environment is the responsibility of the interface or view. The view can be seen as expressing the semantics for the 'glue' that joins components or objects together to create a software system. Informal versions of the views model have already been successfully applied to operational and commercial software systems. The objective of this thesis is to provide the views notion with a theoretical foundation to address reuse and separation of concerns. After clearly defining the views model we show the formal approach to combining the objects, interfaces (views), and their interconnection into a complete software system. The objects and interfaces are defined using an object calculus based on temporal logic, while the interconnections among object and views are specified using category theory. This formal framework provides the mathematical foundation to support the verification of the properties of both the components and the composite software system. We then show how verification can be mechanized by converting the formal version of the views model into higher-order logic and using PVS to support mechanical proofs.

Not available / text

Mechanized theorem proving is a promising means of formally establishing facts about complex systems. However, in applying theorem proving methodologies to industrial-scale hardware and software systems, a large amount of user interaction is required in order to prove useful properties. In practice, the human user tasked with such a verification must gain a deep understanding of the system to be verified, and prove numerous lemmas in order to allow the theorem proving program to approach a proof of the desired fact. Furthermore, proofs that fail during this process are a source of confusion: the proof may either fail because the conjecture was false, or because the prover required more help from the user in order to reach the desired conclusion. We have implemented a symbolic execution framework inside the ACL2 theorem prover in order to help address these issues on certain problem domains. Our framework introduces a proof strategy that applies bit-level symbolic execution using BDDs to finite-domain problems. This proof strategy is a fully verified decision procedure for such problems, and on many useful problem domains its capacity vastly exceeds that of exhaustive testing. Our framework also produces counterexamples for conjectures that it determines to be false. Our framework seeks to reduce the amount of necessary user interaction in proving theorems about industrial-scale hardware and software systems. By increasing the automation available in the prover, we allow the user to complete useful proofs while understanding less of the detailed implementation of the system. Furthermore, by producing counterexamples for falsified conjectures, our framework reduces the time spent by the user in trying to determine why a proof failed. / text

Formal methods is a discipline of using a collection of mathematical techniques and formalisms to model and analyze software systems. Motivated by the new formal methods-based certification recommendations for safety-critical embedded software and the significant increase in the cost of verification and validation (V\&V), this research is about creating a software development process for control systems that can provide mathematical guarantees of high-level functional properties on the code. The process, dubbed credible autocoding, leverages control theory in the automatic generation of control software documented with proofs of their stability and performance. The main output of this research is an automated, credible autocoding prototype that transforms the Simulink model of the controller into C code documented with a code-level proof of the stability of the controller. The code-level proof, expressed using a formal specification language, are embedded into the code as annotations. The annotations guarantee that the auto-generated code conforms to the input model to the extent that key properties are satisfied. They also provide sufficient information to enable an independent, automatic, formal verification of the auto-generated controller software.

The complex behavior of computer systems offers many challenges for formal verification. The analysis quickly becomes difficult as the number of participating processes increases. A parameterized system is a family of systems parameterized on a number n, typically representing the number of participating processes. The uniform verification problem — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general. In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called regular model checking (RMC). In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation. We extend the automata-theoretic approach to RMC. We define a specification logic sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model. We develop acceleration techniques for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature. We present a novel reachability based verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results. Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.

L'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et la prévention des erreurs de conception, dès les premières phases du développement. Ce besoin est motivé par les coûts et délais des phases de vérification et validation. De nombreuses méthodes de spécification, tant formelles qu'informelles ont été proposées et, comme nous le verrons dans cette thèse, les approches formelles donnent des spécifications de meilleure qualité.L'ingénierie des systèmes sécurisés propose l'utilisation de modèles de conception de la sécurité pour représenter les applications sécurisées. Dans de nombreux cas, ces modèles se basent sur les notations graphiques d'UML avec des extensions, sous forme de profils comme SecureUML, pour exprimer la sécurité. Néanmoins, les notations d'UML, même étendues avec des assertions OCL, sont insuffisantes pour garantir la correction de ces modèles. Ceci est notamment du aux limites des outils d'animation utilisés pour valider des modèles UML étendus en OCL. Nous proposons de combiner des langages formels comme Z avec UML pour valider des applications en animant leurs spécifications, indépendamment de futurs choix d'implémentation. Le but de cette thèse est de présenter une approche pour analyser par animation des modèles de conception de la sécurité. Nous utilisons un outil pré-existant, RoZ, pour traduire les aspects fonctionnels du modèle UML en Z. Cependant, RoZ ne couvre pas la modélisation des aspects sécuritaires. Dans cette thèse, nous avons complété l'outil RoZ en l'associant à un noyau de sécurité qui spécifie les concepts du modèle RBAC (Role Based Access Control). Nous utilisons l'animation pour explorer dynamiquement et ainsi valider les aspects sécuritaires de l'application.Notre approche et les outils qui la supportent intègrent UML, SecureUML (un langage de modélisation de la sécurité), RBAC, RoZ, Z et Jaza, un animateur pour le langage Z. L'animation des spécifications prend la forme de scénarios définis par l'utilisateur qui permettent de se convaincre que la spécification décrit correctement ses besoins. Notre approche permet une validation dès la phase de spécification, qui prend en considération l'interaction entre les modèles fonctionnel et sécuritaire, et qui fait abstraction des choix de l'implémentation. Les éléments du modèle fonctionnel peuvent être utilisés comme contexte dans la définition des permissions du modèle de sécurité. Notre approche ne met pas de contrainte sur ce modèle fonctionnel ce qui permet de l'utiliser pour une vaste gamme d'applications.