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.

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.

Un système GALS (Globalement Asynchrone, Localement Synchrone) est un ensemble de composants synchrones qui évoluent en même temps, chacun à propre rythme, et qui communiquent de manière asynchrone. Cette thèse propose un environnement formel de modélisation et de vérification dédié aux systèmes GALS, en se focalisant sur le comportement asynchrone.Notre environnement s’appuie sur un langage formel que nous avons conçu nommé GRL (GALS Représentation Language). GRL permet la spécification comportementale des composants synchrones, de la communication asynchrone, et des contraintes sur les rythmes des composants ainsi que sur les valeurs que prennent les entrées des composants. Pour analyser les spécifications GRL, nous utilisons CADP, une boîte à outils logicielle permettant la vérification de processus concurrents asynchrones par des techniques d'exploration d’espaces d’états. Dans ce but, nous avons défini une traduction de GRL vers LNT, un langage de spécification supporté par CADP. La traduction est implémentée dans un outil appelé GRL2LNT, permettant ainsi la génération automatique d’espaces d'états à partir de spécifications GRL.Pour permettre la vérification formelle des spécifications GRL, nous avons conçu un langage de propriétés nommé muGRL, qui est interprété sur les espaces d’états de GRL. Le langage muGRL est basé sur un ensemble de patrons qui capturent les propriétés des systèmes concurrents et des systèmes GALS, réduisant ainsi la complexité d'utiliser les logiques temporelles classiques. La sémantique de muGRL est définie par traduction vers MCL, le langage de logique temporelle fourni par CADP. Enfin, nous illustrons l’usage de GRL, muGRL et CADP pour la modélisation et la vérification d’applications GALS concrètes, comprenant des études de cas industrielles. / A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronouscomponents that evolve concurrently, each with its own pace, and communicatealtogether asynchronously. This thesis proposes a formal modelling and verificationframework dedicated to GALS systems, with a focus on the asynchronous behaviour.As a cornerstone of our framework, we have designed a formal language, named GRL(GALS Representation Language). GRL enables the behavioural specification of synchronouscomponents, asynchronous communication, and constraints involving bothcomponent paces and the data carried by component inputs. To analyse GRL specifications,we took advantage of the CADP software toolbox for the verification of asynchronousconcurrent processes, using state space exploration techniques. For this purpose,we defined a translation from GRL to the LNT specification language supportedby CADP. The translation was implemented by a tool named GRL2LNT, thus enablingstate spaces to be automatically derived from GRL specifications.To enable the formal verification of GRL specifications, we designed a property specificationlanguage, named muGRL, which is interpreted on GRL state spaces. The muGRLlanguage is based on a set of patterns capturing properties of concurrent and GALSsystems, which reduces the complexity of using full-fledged temporal logics. The semanticsof muGRL are defined by a translation into the MCL temporal logic supported byCADP. Finally, we illustrated how GRL, muGRL, and CADP can be applied to modeland verify concrete GALS applications, including industrial case-studies.