Formal methods are necessary in achieving correct software: that is, software that can be proven to fulfil its requirements. Formal specifications are unambiguous and analysable. Building a formal model improves understanding. The modelling of nondeterminism, and its subsequent removal in formal steps, allows design and implementation decisions to be made when most suitable. Formal models are amenable to mathematical manipulation and reasoning, and facilitate rigorous testing procedures. However, formal methods are not widely used in software development. In most cases, this is because they are not suitably supported with development tools. Further, many software developers do not recognise the need for rigour. Object oriented techniques are successful in the production of large, complex software systems. The methods are based on simple mathematical models of abstraction and classifi cation. Further, the object oriented approach offers a conceptual consistency across all stages of software development. However, the inherent flexibility of object oriented approaches can lead to an incremental and interactive style of development, a consequence of which may be insuffi cient rigour. This lack of rigour is exacerbated by the inconsistent and informal semantics for object oriented concepts at all stages of development. Formal and object oriented methods are complementary in software development: object oriented methods can be used to manage the construction of formal models and formality can add rigour to object oriented software development. This thesis shows how formal object oriented development can proceed from analysis and requirements capture to design and implementation. A formal object oriented analysis language is defined in terms of a state transition system semantics. This language is said to be customer-oriented: a number of graphical views of object oriented relations in the formal analysis models are presented, and the specifi cations produced say what is required rather than how the requirements are to be met. A translation to ACT ONE provides an executable model for customer validation. This translation is founded on a precise statement of the relationship between classes and types (and subclassing and subtypes). The structure of the resulting ACT ONE requirements model corresponds to the structure of the problem domain, as communicated by the customer. The step from analysis to design requires an extension to the requirements model to incorporate semantics for object communication. A process algebra provides a suitable formal model for the specifi cation of communication properties. LOTOS, which combines ACT ONE and a process algebra in one coherent semantic model, provides a means of constructing object oriented design semantics. Design is de fined as the process of transforming a customer-oriented requirements model to an implementation-oriented design, whilst maintaining correctness. Correctness preserving transformations (CPTs) are defined for: transferring requirements structure to design structure, manipulating design structure and changing internal communication models. Design must be targetted towards a particular implementation environment. The thesis examines a number of different environments for the implementation of object oriented LOTOS designs. It illustrates the importance of understanding programming language semantics. We show how Eiffel can be used to implement formal object oriented designs. A case study which evaluates the formal object oriented models and methods, developed in this thesis, is reported. This identifi es re-use at all stages of software development and emphasises the role of structure: it improves understanding and communication, and makes validation and veri fication easier and better. The thesis shows that formal object oriented technology is ready for transfer to industry. These methods should be exploited sooner rather than later: object oriented development can incorporate formal methods without signi ficant cost, and formal methods can utilise the object oriented paradigm to manage complexity. The thesis provides a rationale for formal object oriented development and a set of conceptual tools which makes the development of software systems a true engineering discipline.

O aumento crescente da complexidade dos sistemas computacionais criou a necessidade do uso de técnicas de descrição formal (TDFs) na definição, implementação e manutenção dos sistemas. Contudo, apenas a existência de técnicas de descrição formal não garante o eficiente emprego das mesmas na especificação dos sistemas. É necessária a existência de ferramentas que viabilizem o uso das TDFs de forma que estas possam ser efetivamente úteis no desenvolvimento de projetos. Este trabalho apresenta os resultados obtidos da construção de um ambiente de especificação gráfico, onde a TDF E-LOTOS (Enhancements to LOTOS) fornece os mecanismos que uma técnica de descrição deve possuir para viabilizar a consistência, verificação e validação de sistemas. A TDF é suportada através do emprego de uma nova versão gráfica para a sintaxe textual padrão de E-LOTOS. O principal objetivo deste trabalho é disponibilizar aos projetistas e desenvolvedores um ambiente de especificação onde a criação, implementação, teste e manutenção de sistemas sejam feitos de forma fácil, rápida, intuitiva e consistente. Para tal, uma nova sintaxe gráfica de E-LOTOS foi criada: o E-DART (Enhancements to DART). Foi desenvolvida também uma ferramenta que permite o uso de E-DART, o Editor E-DART. A nova sintaxe abstrai, através de diagramas, as complexidades naturais de E-LOTOS, permitindo uma compreensão mais intuitiva dos sistemas. Com o uso de E-DART as especificações construídas são validadas por uma TDF sem que o processo de criação torne-se complexo. No Editor E-DART, a rapidez na criação das especificações é alcançada com mecanismos de reuso de módulos, e com o emprego de recursos avançados de interação com o usuário. O reuso de módulos diminui o tempo total dispensado na criação de especificações porque as mesmas poderão utilizar partes já homologadas de outros sistemas, sem a necessidade de validação e testes, pois estes são procedimentos realizados anteriormente nas outras especificações. Os recursos avançados de interação, por outro lado, permitem que projetistas não familiarizados com E-LOTOS sejam ainda assim capazes de construir sistemas complexos. Além disso, profissionais que tenham experiência com a TDF têm acesso direto ao código textual E-LOTOS, o que lhes garante uma maior compreensão das especificações. / The increasing complexity of the computational systems has created the necessity of the use of formal description techniques (FDTs) in the systems definition, implementation and maintenance. However, only the existence of formal description techniques does not guarantee their efficient use in the systems specification. The existence of tools is necessary to make the use of the TDFFs possible in a way in which these techniques can be effectively useful in projects development. This work presents the results of the construction of a specification graphical environment, where E-LOTOS FDT (Enhancements to LOTOS) supplies the mechanisms that a description technique must possess to make possible the consistency, verification and validation of systems. The FDT is supported through the use of a new graphical version for the standard textual E-LOTOS syntax. The main goal of this work is to provide to designers and developers a specification environment where the creation, implementation, test and maintenance of systems are made in a easy form, fast, intuitive and consistent way. For such, a new graphical syntax of E-LOTOS was created: the E-DART (Enhancements to DART). A tool that allows the E-DART use was also developed, the E-DART Editor. The new syntax represents, through diagrams, the natural complexities of E-LOTOS, allowing a intuitive understanding of the systems. With the use of E-DART the specifications are still validated by a FDT, without turning their creation into a complex process. In the E-DART Editor, fast creation of the specifications is achieved with mechanisms of module reuse, and with the use of advanced user interaction resources. The reuse of module diminishes the total time used in the specifications creation because it will be possible to use parts already validated of other systems. The advanced interaction resources, on the other hand, allow that designers not familiarized with E-LOTOS to be able to construct complex systems. Moreover, professionals who have experience with the FDT have direct access to textual ELOTOS code, which guarantees an easier understanding of the specifications.

LOTOS (Language Of Temporal Ordering Specification) est un langage <br />de description de systemes paralleles communicants, normalise par l'ISO et le <br />CCITT afin de permettre la definition formelle des protocoles et des services<br />de telecommunications. Le langage utilise des types abstraits algebriques pour<br />specifier les donnees et un calcul de processus proche de CSP et CCS pour<br />exprimer le controle. <br /><br /> Cette these propose une technique de compilation permettant de traduire <br />un sous-ensemble significatif de LOTOS vers un modele reseau de Petri<br />interprete (pouvant servir a produire du code executable) puis vers un<br />modele automate d'etats finis (permettant la verification formelle de programmes<br />LOTOS soit par reduction ou comparaison modulo des relations d'equivalence, soit<br />par evaluation de formules de logiques temporelles).<br /><br /> La methode employee differe des approches usuelles basees sur la<br />reecriture de termes, qui construisent directement le graphe d'etats<br />correspondant a un programme LOTOS. <br /> Ici au contraire la traduction est effectuee en trois etapes successives<br />(expansion, generation et simulation) s'appuyant sur des modeles semantiques<br />intermediaires (le langage SUBLOTOS et le modele reseau). Elle met en oeuvre<br />une analyse statique globale du comportement des programmes.<br /> Elle prend en compte les donnees, celles-ci devant etre compilees<br />au moyen dalgorithmes deja existants.<br /><br /> Ces principes de compilation ont ete entierement implementes dans<br />le logiciel CAESAR. Les performances obtenues confirment l'interet de la methode.

Stuttgart, Univ., Fakultät Informatik, Diplomarb., 1998.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnologico / Made available in DSpace on 2016-01-08T20:40:04Z (GMT). No. of bitstreams: 1 108166.pdf: 4266376 bytes, checksum: 928d643e8dfa7a47bbad3966c456e640 (MD5) Previous issue date: 1996 / Esta dissertação apresenta uma abordagem para o projeto de sistemas de gerência de redes de computadores que emprega uma biblioteca de construções predefinidas (a biblioteca bibLOTOS), realizadas com o uso da Técnica de Descrição Formal LOTOS. A biblioteca, implementada em banco de Dados ACCESS 2.0, inclui construções em LOTOS Básico, ACT ONE e LOTOS Completo. O emprego da bibLOTOS, assim como do método a ela associado, são ilustrados com o projeto de um sistema de gerência proativa de redes. Ferramentas LOTOS são utilizadas para a validação das especificações.

O aumento crescente da complexidade dos sistemas computacionais criou a necessidade do uso de técnicas de descrição formal (TDFs) na definição, implementação e manutenção dos sistemas. Contudo, apenas a existência de técnicas de descrição formal não garante o eficiente emprego das mesmas na especificação dos sistemas. É necessária a existência de ferramentas que viabilizem o uso das TDFs de forma que estas possam ser efetivamente úteis no desenvolvimento de projetos. Este trabalho apresenta os resultados obtidos da construção de um ambiente de especificação gráfico, onde a TDF E-LOTOS (Enhancements to LOTOS) fornece os mecanismos que uma técnica de descrição deve possuir para viabilizar a consistência, verificação e validação de sistemas. A TDF é suportada através do emprego de uma nova versão gráfica para a sintaxe textual padrão de E-LOTOS. O principal objetivo deste trabalho é disponibilizar aos projetistas e desenvolvedores um ambiente de especificação onde a criação, implementação, teste e manutenção de sistemas sejam feitos de forma fácil, rápida, intuitiva e consistente. Para tal, uma nova sintaxe gráfica de E-LOTOS foi criada: o E-DART (Enhancements to DART). Foi desenvolvida também uma ferramenta que permite o uso de E-DART, o Editor E-DART. A nova sintaxe abstrai, através de diagramas, as complexidades naturais de E-LOTOS, permitindo uma compreensão mais intuitiva dos sistemas. Com o uso de E-DART as especificações construídas são validadas por uma TDF sem que o processo de criação torne-se complexo. No Editor E-DART, a rapidez na criação das especificações é alcançada com mecanismos de reuso de módulos, e com o emprego de recursos avançados de interação com o usuário. O reuso de módulos diminui o tempo total dispensado na criação de especificações porque as mesmas poderão utilizar partes já homologadas de outros sistemas, sem a necessidade de validação e testes, pois estes são procedimentos realizados anteriormente nas outras especificações. Os recursos avançados de interação, por outro lado, permitem que projetistas não familiarizados com E-LOTOS sejam ainda assim capazes de construir sistemas complexos. Além disso, profissionais que tenham experiência com a TDF têm acesso direto ao código textual E-LOTOS, o que lhes garante uma maior compreensão das especificações. / The increasing complexity of the computational systems has created the necessity of the use of formal description techniques (FDTs) in the systems definition, implementation and maintenance. However, only the existence of formal description techniques does not guarantee their efficient use in the systems specification. The existence of tools is necessary to make the use of the TDFFs possible in a way in which these techniques can be effectively useful in projects development. This work presents the results of the construction of a specification graphical environment, where E-LOTOS FDT (Enhancements to LOTOS) supplies the mechanisms that a description technique must possess to make possible the consistency, verification and validation of systems. The FDT is supported through the use of a new graphical version for the standard textual E-LOTOS syntax. The main goal of this work is to provide to designers and developers a specification environment where the creation, implementation, test and maintenance of systems are made in a easy form, fast, intuitive and consistent way. For such, a new graphical syntax of E-LOTOS was created: the E-DART (Enhancements to DART). A tool that allows the E-DART use was also developed, the E-DART Editor. The new syntax represents, through diagrams, the natural complexities of E-LOTOS, allowing a intuitive understanding of the systems. With the use of E-DART the specifications are still validated by a FDT, without turning their creation into a complex process. In the E-DART Editor, fast creation of the specifications is achieved with mechanisms of module reuse, and with the use of advanced user interaction resources. The reuse of module diminishes the total time used in the specifications creation because it will be possible to use parts already validated of other systems. The advanced interaction resources, on the other hand, allow that designers not familiarized with E-LOTOS to be able to construct complex systems. Moreover, professionals who have experience with the FDT have direct access to textual ELOTOS code, which guarantees an easier understanding of the specifications.

O aumento crescente da complexidade dos sistemas computacionais criou a necessidade do uso de técnicas de descrição formal (TDFs) na definição, implementação e manutenção dos sistemas. Contudo, apenas a existência de técnicas de descrição formal não garante o eficiente emprego das mesmas na especificação dos sistemas. É necessária a existência de ferramentas que viabilizem o uso das TDFs de forma que estas possam ser efetivamente úteis no desenvolvimento de projetos. Este trabalho apresenta os resultados obtidos da construção de um ambiente de especificação gráfico, onde a TDF E-LOTOS (Enhancements to LOTOS) fornece os mecanismos que uma técnica de descrição deve possuir para viabilizar a consistência, verificação e validação de sistemas. A TDF é suportada através do emprego de uma nova versão gráfica para a sintaxe textual padrão de E-LOTOS. O principal objetivo deste trabalho é disponibilizar aos projetistas e desenvolvedores um ambiente de especificação onde a criação, implementação, teste e manutenção de sistemas sejam feitos de forma fácil, rápida, intuitiva e consistente. Para tal, uma nova sintaxe gráfica de E-LOTOS foi criada: o E-DART (Enhancements to DART). Foi desenvolvida também uma ferramenta que permite o uso de E-DART, o Editor E-DART. A nova sintaxe abstrai, através de diagramas, as complexidades naturais de E-LOTOS, permitindo uma compreensão mais intuitiva dos sistemas. Com o uso de E-DART as especificações construídas são validadas por uma TDF sem que o processo de criação torne-se complexo. No Editor E-DART, a rapidez na criação das especificações é alcançada com mecanismos de reuso de módulos, e com o emprego de recursos avançados de interação com o usuário. O reuso de módulos diminui o tempo total dispensado na criação de especificações porque as mesmas poderão utilizar partes já homologadas de outros sistemas, sem a necessidade de validação e testes, pois estes são procedimentos realizados anteriormente nas outras especificações. Os recursos avançados de interação, por outro lado, permitem que projetistas não familiarizados com E-LOTOS sejam ainda assim capazes de construir sistemas complexos. Além disso, profissionais que tenham experiência com a TDF têm acesso direto ao código textual E-LOTOS, o que lhes garante uma maior compreensão das especificações. / The increasing complexity of the computational systems has created the necessity of the use of formal description techniques (FDTs) in the systems definition, implementation and maintenance. However, only the existence of formal description techniques does not guarantee their efficient use in the systems specification. The existence of tools is necessary to make the use of the TDFFs possible in a way in which these techniques can be effectively useful in projects development. This work presents the results of the construction of a specification graphical environment, where E-LOTOS FDT (Enhancements to LOTOS) supplies the mechanisms that a description technique must possess to make possible the consistency, verification and validation of systems. The FDT is supported through the use of a new graphical version for the standard textual E-LOTOS syntax. The main goal of this work is to provide to designers and developers a specification environment where the creation, implementation, test and maintenance of systems are made in a easy form, fast, intuitive and consistent way. For such, a new graphical syntax of E-LOTOS was created: the E-DART (Enhancements to DART). A tool that allows the E-DART use was also developed, the E-DART Editor. The new syntax represents, through diagrams, the natural complexities of E-LOTOS, allowing a intuitive understanding of the systems. With the use of E-DART the specifications are still validated by a FDT, without turning their creation into a complex process. In the E-DART Editor, fast creation of the specifications is achieved with mechanisms of module reuse, and with the use of advanced user interaction resources. The reuse of module diminishes the total time used in the specifications creation because it will be possible to use parts already validated of other systems. The advanced interaction resources, on the other hand, allow that designers not familiarized with E-LOTOS to be able to construct complex systems. Moreover, professionals who have experience with the FDT have direct access to textual ELOTOS code, which guarantees an easier understanding of the specifications.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL.

La vérification formelle est indispensable pour assurer la fiabilité des applications critiques comme les protocoles de communication et les systèmes répartis. La technique de vérification basée sur les modèles (model-checking) consiste à traduire l'application vers un système de transitions étiquetées (STE), sur lequel les propriétés attendues, exprimées en logique temporelle, sont vérifiées à l'aide d'outils appelés évaluateurs (model-checkers). Cependant, les logiques temporelles "classiques", définies sur un vocabulaire d'actions atomiques, ne sont pas adaptées aux langages de description comme LOTOS, dont les actions contiennent des valeurs typées. Cette thèse définit un formalisme appelé XTL (eXecutable Temporal Language) qui permet d'exprimer des propriétés temporelles portant sur les données du programme à vérifier. XTL est basé sur une extension du mu-calcul modal avec des variables typées. Les valeurs contenues dans le STE, extraites à l'aide d'opérateurs modaux étendus, peuvent être passées en paramètre aux opérateurs de point fixe ou manipulées à l'aide de constructions d'inspiration fonctionnelle comme "let", "if-then-else", "case", etc. Les propriétés portant sur des séquences d'actions du programme sont décrites succinctement au moyen d'expressions régulières. Des méta-opérateurs spéciaux permettent l'évaluation des formules sur un STE et l'expression de propriétés temporelles non-standard par exploration de la relation de transition. La sémantique de XTL est formellement définie et des algorithmes efficaces sont proposés pour évaluer des formules temporelles XTL sur des modèles STEs. Un évaluateur XTL est développé et utilisé avec succès pour la validation d'applications industrielles comme le protocole BRP développé par Philips et la couche liaison du bus série IEEE-1394 ("FireWire").

Cette thèse porte sur la vérification formelle de systèmes temps réel et procède par transformation de modèle entre l'algèbre de processus temporisée RT-LOTOS et les réseaux de Petri temporels étendus par des chronomètres et des données. Des schémas de traduction de RT-LOTOS vers ces réseaux de Petri étendus sont proposés et formellement prouvés. L'approche transformationnelle développée pour la partie " contrôle " de RT-LOTOS est étendue à la partie " données ". Le langage RT-LOTOS est lui même enrichi d'un opérateur de suspension reprise qui permet de modéliser et vérifier une classe plus large de systèmes temps réel Plusieurs études de cas attestent de l'efficacité des schémas de traduction proposés par rapport à des outils LOTOS ou RT-LOTOS développés antérieurement. L'approche proposée s'avère transposable à d'autres langages de modélisation en particulier le profil UML temps réel TURTLE (Timed UML and RT-LOTOS Environment).