Network protocol construction is a complex and error prone task. The challenges originate both from the inherent complexity of developing correct program code and from the distributed nature of networked systems. Protocol errors can have devastating consequences. Even so, methods for ensuring protocol correctness are currently only used to a limited extent. A central reason for this is that they are often complex and expensive to employ. In this thesis, we develop methods to perform network protocol testing and verification, with the goal to make the techniques more accessible and readily adoptable. We examine how to formulate correctness requirements for ad hoc routing protocols used to set up forwarding paths in wireless networks. Model checking is a way to verify such requirements automatically. We investigate scalability of finite-state model checking, in terms of network size and topological complexity, and devise a manual abstraction technique to improve scalability. A methodology combining simulations, emulations, and real world experiments is developed for analyzing the performance of wireless protocol implementations. The technique is applied in a comparison of the ad hoc routing protocols AODV, DSR, and OLSR. Discrepancies between simulations and real world behavior are identified; these are due to absence of realistic radio propagation and mobility models in simulation. The issues are mainly related to how the protocols sense their network surroundings and we identify improvements to these capabilities. Finally, we develop a methodology and a tool for automatic verification of safety properties of infinite-state network protocols, modeled as graph transformation systems extended with negative application conditions. The verification uses symbolic backward reachability analysis. By introducing abstractions in the form of summary nodes, the method is extended to protocols with recursive data structures. Our tool automatically verifies correct routing of the DYMO ad hoc routing protocol and several nontrivial heap manipulating programs.

Communicating Sequential Processes (CSP) is a formal language whose primary purpose is to model and verify concurrent systems. The CSP++ toolset was created to embody the concept of selective formalism by making machine-readable CSPm specifications both executable (through the automatic synthesis of C++ source) and extensible (by allowing the integration of C++ user-coded functions). However, these user-coded functions were limited by their inability to share data with each other, which meant that their application was constrained to solving simple problems in isolation. We extend CSP++ by providing user-coded functions in the same CSP process with safe access to a shared storage area, similar in concept and API to Pthreads' thread-local storage, enabling cooperation between them and granting them the ability to undertake more complex tasks without breaking the formalism of the underlying specification. This feature's utility is demonstrated in our line-following robot case study.

Change management is a discipline fundamental to the task of building ever more complex computing systems. Properly managed change provides a means whereby alterations to existing components of a complex artefact and their relationships can be evaluated, managed and evolved. This thesis takes as its example Official RAAF Publications, some of which need to be revised as a result of changes to the system they describe. The thesis develops a model of change propagation providing a set of operations to examine and record the changes to a set of publications. Additional operations enable coping with reversing decisions and handling the unexpected arrival of externally generated amendments. The model is extended to cover a finer granularity of entities (at the page level) to determine whether this greater level of detail would ease some tasks. A further extension provides the notion of relationships between the publications of concern, focusing on a dependency relationship between two publications. This enables exploration of the possibility of improving the process by reducing the risk of missing publications needing revision and providing a means by which some tasks can be partly automated thus speeding up the process. The models presented were developed in Sum, a variant of the Z specification language, to gain greater insight into the essential details of the operations and data structures involved. By ignoring implementation details the essential logical steps of each model can be emphasised and their differences and similarities contrasted. This thesis demonstrates that fine-grained change management is feasible. The thesis develops processes that automatically track the status of changes as they are propagated through a set of documents. The greater knowledge of work done on individual pages allows only the page(s) of concern to be affected. The work also enables recommendations to be made as to the applicability of each model and, by comparing the models, provides insight into the amount of work and resources required for tackling change at different levels of granularity.

Change management is a discipline fundamental to the task of building ever more complex computing systems. Properly managed change provides a means whereby alterations to existing components of a complex artefact and their relationships can be evaluated, managed and evolved. This thesis takes as its example Official RAAF Publications, some of which need to be revised as a result of changes to the system they describe. The thesis develops a model of change propagation providing a set of operations to examine and record the changes to a set of publications. Additional operations enable coping with reversing decisions and handling the unexpected arrival of externally generated amendments. The model is extended to cover a finer granularity of entities (at the page level) to determine whether this greater level of detail would ease some tasks. A further extension provides the notion of relationships between the publications of concern, focusing on a dependency relationship between two publications. This enables exploration of the possibility of improving the process by reducing the risk of missing publications needing revision and providing a means by which some tasks can be partly automated thus speeding up the process. The models presented were developed in Sum, a variant of the Z specification language, to gain greater insight into the essential details of the operations and data structures involved. By ignoring implementation details the essential logical steps of each model can be emphasised and their differences and similarities contrasted. This thesis demonstrates that fine-grained change management is feasible. The thesis develops processes that automatically track the status of changes as they are propagated through a set of documents. The greater knowledge of work done on individual pages allows only the page(s) of concern to be affected. The work also enables recommendations to be made as to the applicability of each model and, by comparing the models, provides insight into the amount of work and resources required for tackling change at different levels of granularity.

Change management is a discipline fundamental to the task of building ever more complex computing systems. Properly managed change provides a means whereby alterations to existing components of a complex artefact and their relationships can be evaluated, managed and evolved. This thesis takes as its example Official RAAF Publications, some of which need to be revised as a result of changes to the system they describe. The thesis develops a model of change propagation providing a set of operations to examine and record the changes to a set of publications. Additional operations enable coping with reversing decisions and handling the unexpected arrival of externally generated amendments. The model is extended to cover a finer granularity of entities (at the page level) to determine whether this greater level of detail would ease some tasks. A further extension provides the notion of relationships between the publications of concern, focusing on a dependency relationship between two publications. This enables exploration of the possibility of improving the process by reducing the risk of missing publications needing revision and providing a means by which some tasks can be partly automated thus speeding up the process. The models presented were developed in Sum, a variant of the Z specification language, to gain greater insight into the essential details of the operations and data structures involved. By ignoring implementation details the essential logical steps of each model can be emphasised and their differences and similarities contrasted. This thesis demonstrates that fine-grained change management is feasible. The thesis develops processes that automatically track the status of changes as they are propagated through a set of documents. The greater knowledge of work done on individual pages allows only the page(s) of concern to be affected. The work also enables recommendations to be made as to the applicability of each model and, by comparing the models, provides insight into the amount of work and resources required for tackling change at different levels of granularity.

Change management is a discipline fundamental to the task of building ever more complex computing systems. Properly managed change provides a means whereby alterations to existing components of a complex artefact and their relationships can be evaluated, managed and evolved. This thesis takes as its example Official RAAF Publications, some of which need to be revised as a result of changes to the system they describe. The thesis develops a model of change propagation providing a set of operations to examine and record the changes to a set of publications. Additional operations enable coping with reversing decisions and handling the unexpected arrival of externally generated amendments. The model is extended to cover a finer granularity of entities (at the page level) to determine whether this greater level of detail would ease some tasks. A further extension provides the notion of relationships between the publications of concern, focusing on a dependency relationship between two publications. This enables exploration of the possibility of improving the process by reducing the risk of missing publications needing revision and providing a means by which some tasks can be partly automated thus speeding up the process. The models presented were developed in Sum, a variant of the Z specification language, to gain greater insight into the essential details of the operations and data structures involved. By ignoring implementation details the essential logical steps of each model can be emphasised and their differences and similarities contrasted. This thesis demonstrates that fine-grained change management is feasible. The thesis develops processes that automatically track the status of changes as they are propagated through a set of documents. The greater knowledge of work done on individual pages allows only the page(s) of concern to be affected. The work also enables recommendations to be made as to the applicability of each model and, by comparing the models, provides insight into the amount of work and resources required for tackling change at different levels of granularity.

Thesis (MSc (Mathematical Sciences))--University of Stellenbosch, 2007. / The ever-increasing reliance of society on computer systems has led to a need for highly reliable systems. There are a number of areas where computer systems perform critical functions and the development of such systems requires a higher level of attention than any other type of system. The appropriate approach in this situation is known as formal methods. Formal methods refer to the use of mathematical techniques for the specification, development and verification of software and hardware systems. The two main goals of this thesis are: 1. The design of mathematical models as a basis for the implementation of error-free software for the safety interlock system at iThemba LABS (http://www.tlabs.ac.za/). 2. The comparison of formal method techniques that addresses the lack of much-needed empirical studies in the field of formal methods. Mathematical models are developed using model checkers: Spin, Uppaal, Smv and a theorem prover Pvs. The criteria used for the selection of the tools was based on the popularity of the tools, support of the tools, representation of properties, representativeness of verification techniques, and ease of use. The procedure for comparing these methods is divided into two phases. Phase one involves the time logging of activities followed by a novice modeler to model check and theorem prove software systems. The results show that it takes more time to learn and use a theorem prover than a model checker. Phase two involves the performance of the tools in relation to the time taken to verify a property, memory used, number of states and transitions generated. In spite of the differences between models, the results are in favor of Smv and this maybe attributed to the nature of the safety interlock system, as it involves a lot of hard-wired lines.

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit / The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems

Made available in DSpace on 2014-12-17T15:47:43Z (GMT). No. of bitstreams: 1 PlacidoASN.pdf: 652214 bytes, checksum: b7912104bf8e3ec91262c75b9ef5d36b (MD5) Previous issue date: 2007-09-06 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler / M?todos formais poderiam ser usados para especificar e verificar software on-card em aplica??es Java Card. O estilo de programa??o para smart cards requer verifica??o em tempo de execu??o para condi??es de entrada em todos os m?todos Java Card, onde o objetivo principal ? preservar os dados do cart?o. Projeto por Contrato, em particular, a linguagem JML, ? uma op??o para este tipo de desenvolvimento e verifica??o, pelo fato da verifica??o em tempo de execu??o ser parte da implementa??o pela JML. Contudo, JML e suas respectivas ferramentas para verifica??o em tempo de execu??o n?o foram projetadas com o foco nas limita??es Java Card, sendo, dessa forma, n?o compat?veis com Java Card. Nesta disserta??o, analisamos o quanto esta situa??o ? realmente intr?nseca ?s limita??es Java Card e, se ? poss?vel re-definir a JML e suas ferramentas. Propomos requisitos para uma nova linguagem, a qual ? compat?vel com Java Card e apresentamos como o compilador desta linguagem pode ser constru?do. JCML retira da JML aspectos n?o definidos em Java Card, como por exemplo, concorr?ncia e tipos n?o suportados. Isto pode n?o ser o bastante, contudo, sem o esfor?o em otimiza??o de c?digo de verifica??o gerado pelo compilador, n?o ? poss?vel gerar c?digo de verifica??o para rodar no cart?o. O compilador JCML, apesar de ser bem mais restrito em rela??o ao compilador JML, est? habilitado a gerar c?digo de verifica??o compat?vel com Java Card, para algumas especifica??es lightweight. Como conclus?o, apresentamos uma variante da JML compat?vel com Java Card, JCML (Java Card Modeling Language), com uma vers?o de seu compilador

Made available in DSpace on 2014-12-17T15:47:44Z (GMT). No. of bitstreams: 1 BrunoEGG.pdf: 1320681 bytes, checksum: 897ca75ef7f0e564e8588d949fcc67d5 (MD5) Previous issue date: 2007-11-19 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures / A tecnologia Java Card permite o desenvolvimento e execu??o de pequenas aplica??es embutidas em smart cards. Uma aplica??o Java Card ? composta por um cliente, externo ao cart?o, e por uma aplica??o contida no cart?o que implementa os servi?os dispon?veis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplica??es manipulam e armazenam informa??es importantes, tais como valores monet?rios ou dados confidenciais do seu portador. Sendo assim, faz-se necess?rio adotar um maior rigor no processo de desenvolvimento de uma aplica??o smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de m?todos formais como parte desse processo ? um meio de se alcan?ar esses requisitos de qualidade. O m?todo formal B ?e um dentre os diversos m?todos formais para a especifica??o de sistemas. O desenvolvimento em B tem in?cio com a especifica??o funcional do sistema, continua com a aplica??o opcional de refinamentos ? especifica??o e, a partir do ?ltimo n?vel de refinamento, ? poss?vel a gera??o de c?digo para alguma linguagem de programa??o. O formalismo B conta com bom suporte de ferramentas e a sua aplica??o a Java Card mostra-se bastante adequada, uma vez que a especifica??o e desenvolvimento de APIs ?e o ponto forte de B. O m?todo BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplica??es Java Card a partir da gera??o de c?digo da aplica??o com base em refinamentos da sua especifica??o formal descrita na nota??o B. O processo de desenvolvimento descrito no m?todo ? apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do m?todo; e por uma biblioteca de m?dulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutiliz?veis