Biblioteca Digital

O desenvolvimento de arquiteturas de controle para veículos submarinos é uma tarefa complexa. Estas podem ser caracterizadas pelos seguintes atributos: tempo real, multitarefa, concorrência e comunicações distribuídas em rede. Neste cenário, existem múltiplos processos sendo executados em paralelo, possivelmente distribuídos, e se comunicando uns com os outros. Neste contexto, o modelo comportamental pode levar a fenômenos como deadlocks, livelocks, disputa por recursos, entre outros. A fim de se tentar minimizar os efeitos de tais dificuldades, neste trabalho será apresentado um método para checagem de modelos de arquiteturas de controle de veículos submarinos baseado em Especificações Formais. A linguagem de especificação formal escolhida foi CSP-OZ, uma combinação de CSP e Object-Z. Object-Z é uma extensão orientada a objetos da linguagem Z para a especificação de predicados, tipicamente pré e pós condições, além de invariantes de dados. CSP (Communicating Sequential Process) é uma álgebra de processos desenvolvida para descrever modelos comportamentais de processos paralelos. A checagem de modelos especificados formalmente consiste na análise das especificações para verificar se um sistema possui certas propriedades através de uma busca exaustiva em todos os estados em que este pode entrar durante sua execução. Neste contexto...

Prosoft é um grupo de pesquisa do Instituto de Informática da UFRGS, desenvolvido pelo grupo de pesquisa homônimo e coordenado pelo Professor Daltro José Nunes. O objetivo do projeto é desenvolver um ambiente de desenvolvimento de software completo, o Ambiente Prosoft, que é baseado nos conceitos de Modelos, Cálculo Lambda, Tipos Abstratos de Dados e Orientação a Objetos. Um dos componentes do Ambiente Prosoft é sua linguagem de especificação algébrica: o Prosoft Algébrico. Apesar de ser base e tema de diversos trabalhos no grupo de pesquisa Prosoft, o Prosoft Algébrico não tem sua semântica devidamente definida. Os trabalhos desenvolvidos até agora foram baseados em noções operacionais, e apresentam diferentes interpretações do Prosoft Algébrico. Esta dissertação apresenta uma especificação de semântica denotacional para o Prosoft Algébrico, compreendendo, entre outras características, sua primitiva de comunicação entre tipos de dados, chamada ICS, e sua notação gráfica para representação de instanciação de tipos abstratos de dados. Essa dissertação apresenta também um estudo sobre prototipação semântica usando a linguagem de programação Haskell. O conceito de Literate Programming e a proximidade entre Cálculo Lambda e Haskell foram cruciais no rápido desenvolvimento de uma implementação protótipo do Prosoft Algébrico...

A especificação abstrata de tipos de dados, a hoje um dos conceitos mais importantes, aceitos e compreendidos da Ciência da Computação, que permite descrever as principais entidades de um sistema baseado em computador através das propriedades que tais entidades devem satisfazer. Isto a feito usando métodos e linguagens algébricos, onde as propriedades são definidas na forma de axiomas (equações). Por outro lado, a tecnologia chamada de Orientada a Objetos (00), foi se transformando em uma disciplina amadurecida para projetos e implementações de aplicações de software. Atualmente esta tecnologia inclui muitas metodologias e muitas linguagens que abrangem todo o processo de desenvolvimento de sistemas, porem, a maioria delas são influenciadas pela implementação de tais sistemas, isto e, os conceitos básicos 00 de classe, objeto e herança são definidos em fungi° da linguagem de implementação a ser usada. Alem disso, notamos que nos últimos anos esta sendo desenvolvida muita pesquisa sobre uma geração de computadores que envolvem massivamente arquiteturas paralelas (computação concorrente), bem como sobre sistemas de comunicação de dados e engenharia (descrição) de protocolos. O objetivo principal desta tese a dar uma resposta a estes três assuntos integrando três conceitos básicos da Engenharia de Software: Especificação Algébrica...

A abordagem de sistemas multiagentes tem sido cada vez mais utilizada para o desenvolvimento de sistemas complexos, o que despertou o interesse das pesquisas na área de engenharia de software orientada a agentes (AOSE) e modelos organizacionais. Neste contexto, esta tese estuda a aplicabilidade de alguns métodos formais tradicionais de engenharia de software para a especificação formal de organizações de sistemas multiagentes, analisando o uso da linguagem de especificação formal RSL para representar o modelo organizacional PopOrg. A escolha da linguagem RSL ocorreu pelo fato de ela ser uma linguagem de especificação formal que cobre amplo espectro de métodos de especificação formal (baseados em modelos e baseados em propriedades, aplicativos e imperativos, sequenciais e concorrentes) e o modelo PopOrg foi escolhido por ser um modelo mínimo de organização de sistemas multiagentes, concebido para representar o conjunto mínimo de aspectos estruturais e operacionais que tais organizações devem ter. O uso da linguagem RSL foi avaliado tanto para a especificação do aspecto estrutural dos sistemas PopOrg, quanto para especificação operacional desses sistemas. Um estudo preliminar realizado com a linguagem CSP para a especificação operacional do modelo PopOrg também é apresentado...

Vários sistemas de grid e computação distribuída existentes só permitem a execução de aplicações com um fluxo de execução de tarefas básico, no qual é feita a distribuição das tarefas executadas em paralelo e depois a coleta de seus resultados. Outros sistemas permitem definir uma relação de dependências entre as tarefas, formando um grafo direcionado acíclico. Porém, mesmo com este modelo de fluxo de execução não é possível executar vários tipos de aplicações que poderiam ser paralelizadas, como, por exemplo, algoritmos genéticos e de cálculo numérico que utilizam algum tipo de processamento iterativo. Nesta dissertação é proposta uma linguagem de especificação para fluxo de execução de aplicações paralelas que permite um controle de fluxo de tarefas mais flexível, viabilizando desvios condicionais e laços com iterações controladas. A linguagem é baseada na notação XML (eXtensible Markup Language), o que lhe confere características importantes tais como flexibilidade e simplicidade. Para avaliar estas e outras características da linguagem proposta, foi feita uma implementação sobre o sistema de processamento paralelo JoiN. Além de viabilizar a criação e execução de novas aplicações paralelas cujos fluxos de tarefas contêm laços e/ou desvios condicionais...

Poker is used to measure progresses in extensive-form games research due to its unique characteristics: it is a game where playing agents have to deal with incomplete information and stochastic scenarios and a large number of decision points. The development of Poker agents has seen significant advances in one-on-one matches but there are still no consistent results in multiplayer and in games against human experts. In order to allow for experts to aid the improvement of the agents performance, we have created a high-level strategy specification language. To support strategy definition, we have also developed an intuitive graphical tool. Additionally, we have also created a strategy inferring system, based on a dynamically weighted Euclidean distance. This approach was validated through the creation of simple agents and by successfully inferring strategies from 10 human players. The created agents were able to beat previously developed mid-level agents by a good profit margin.

After being able to mark-up text and validate its structure according to a document type specification, we may start thinking it would be natural to be able to validate some nonstructural issues in the documents. This paper is to formally discuss semantic-related aspects. In that context, we introduce a domain specific language developed for such a purpose: XCSL. XCSL is not just a language, it is also a processing model. Furthermore, we discuss the general philosophy underlying the proposed approach, presenting the architecture of our semantic validation system, and we detail the respective processor. To illustrate the use of XCSL language and the subsequent processing, we present two case-studies. Nowadays, we can find some other languages to restrict XML documents to those semantically valid - namely Schematron and XML-Schema. So, before concluding the paper, we compare XCSL to those approaches.

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.; Java Card is a version of Java developed to run on devices with severe storage and processing restrictions. The applets that run on these devices are frequently intended for use in critical,highly distributed, mobile conditions. They are required to be portable and safe. Often, the requirements of the application impose the use of dynamic, on-card verifications, but most of the research developed to improve the safety of Java Card applets concentrates on static verification methods. This work presents a runtime verification approach based on Design by Contract to improve the safety of Java Card applications. To this end, we propose JCML (Java Card Modelling Language) a specification language derived from JML (Java Modelling Language) and its implementation: a compiler that generates runtime verification code. We also present some experiments and quality indicators. This paper extends previous published work from the authors with a more complete and precise definition of the JCML language and new experiments and results.

peer-reviewed; Rich and multifaceted domain specific specification languages like the Autonomic System Specification Language (ASSL) help to design reliable systems with self-healing capabilities. The GEAR game-based Model Checker has been used successfully to investigate properties of the ESA Exo-Mars Rover in depth. We show here how to enable GEAR’s game-based verification techniques for ASSL via systematic model extraction from a behavioral subset of the language, and illustrate it on a description of the Voyager II space mission.

Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. E. Guerra, J. de Lara, D. S. Kolovos, and R. F. Paige, "A Visual Specification Language for Model-to-Model Transformations", 2010 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), Leganes (Spain), 2010, pp- 119 - 126; Model Driven Engineering promotes models as the core assets of projects and hence model transformations become first-class citizens in this approach. Likewise, the development of large scale transformations necessitates a systematic engineering process and supporting modelling notations. However, although many languages have been proposed to implement transformations, few allow their specification at a higher level of abstraction. In this paper we present a visual, formal, declarative specification language to express model-to-model transformations and their correctness properties. The language supports the two main approaches to model-to-model transformation -- trace-based and traceless -- with a unified formal semantics. Moreover...

peer-reviewed; Applying design patterns while developing a software system can improve its non-functional properties, such as extensibility and loose coupling. Precise specification of structure and behaviour communicates the invariants imposed by a pattern on a conforming implementation and enables formal software verification. Many existing design-pattern specification languages (DPSLs) focus on class structure alone, while those that do address behaviour suffer from a lack of expressiveness and/or imprecise semantics. In particular, in a review of existing work, three invariant categories were found to be inexpressible in state-of-the-art DPSLs: dependency, object state and data-structure. This paper presents Alas: a precise specification language that supports design-pattern descriptions including these invariant categories. The language is based on UML Class and Sequence diagrams with modified syntax and semantics. In this paper, the meaning of the presented invariants is formalized and relevant ambiguities in the UML Standard are clarified. We have evaluated Alas by specifying the widely-used Gang of Four pattern catalog and identified patterns that benefitted from the added expressiveness and semantics of Alas.

After being able to mark-up text and validate its structure according to a document's type specification, we may start thinking it would be natural to be able to validate some non-structural issues in the documents. This paper is to formally discuss semantic-related aspects. In that context, we introduce a domain specific language developed for such a purpose: XCSL. XCSL is not just a language, it is also a processing model. Furthermore, we discuss the general philosophy underlying the proposed approach, presenting the architecture of our semantic validation system, and we detail the respective processor. To illustrate the use of XCSL language and the subsequent processing, we present a case-study. Nowadays, we can find some other languages to restrict XML documents to those semantically valid - namely Schematron and XML-Schema. So, before concluding the paper, we compare XCSL to those approaches.; Tendo a possibilidade de anotar texto e validar a sua estrutura de acordo com a especificação do tipo de documento, é natural começar a pensar o quão necessário e importante seria validar aspectos não-estruturais nos documentos. O objectivo deste artigo é, precisamente, discutir formalmente aspectos relacionados com a semântica dos documentos. Nesse contexto...

Within a multilevel secure (MLS) system, trusted subjects are granted privileges to perform operations that are not possible by ordinary subjects controlled by mandatory access control (MAC) policy enforcement mechanisms. These subjects are trusted not to conduct malicious activity or degrade system security. We present a formal definition for trusted subject behaviors, which depends upon a representation of information flow and control dependencies generated during a program execution. We describe a security Domain Model (DM) designed in the Alloy specification language for conducting static analysis of programs to identify illicit information flows, access control flaws and covert channel vulnerabilities. The DM is compiled from a representation of a target program, written in an intermediate Implementation Modeling Language (IML), and a specification of the security policy written in Alloy. The Alloy Analyzer tool is used to perform static analysis of the DM to detect potential security policy violations in the target program. In particular, since the operating system upon which the trusted subject runs has limited ability to control its actions, static analysis of trusted subject operations can contribute to the security of the system.

Recent years have seen an increasing need of high-level specification languages and tools generating code from specifications. In this paper, we introduce a specification language, {\splname}, which is tailored to the writing of syntactic theories of language semantics. More specifically, the language supports specifying primitive notions such as dynamic constraints, contexts, axioms, and inference rules. We also introduce a system which generates interpreters from {\splname} specifications. A prototype system is implemented and has been tested on a number of examples, including a syntactic theory for Verilog.; Comment: Accepted in Rule-based Programming Workshop, 2000, 16 pages

Writing specifications for computer programs is not easy since one has to take into account the disparate conceptual worlds of the application domain and of software development. To bridge this conceptual gap we propose controlled natural language as a declarative and application-specific specification language. Controlled natural language is a subset of natural language that can be accurately and efficiently processed by a computer, but is expressive enough to allow natural usage by non-specialists. Specifications in controlled natural language are automatically translated into Prolog clauses, hence become formal and executable. The translation uses a definite clause grammar (DCG) enhanced by feature structures. Inter-text references of the specification, e.g. anaphora, are resolved with the help of discourse representation theory (DRT). The generated Prolog clauses are added to a knowledge base. We have implemented a prototypical specification system that successfully processes the specification of a simple automated teller machine.; Comment: 16 pages, compressed, uuencoded Postscript, published in Proceedings CLNLP 95, COMPULOGNET/ELSNET/EAGLES Workshop on Computational Logic for Natural Language Processing, Edinburgh, April 3-5...

Deriving formal specifications from informal requirements is difficult since one has to take into account the disparate conceptual worlds of the application domain and of software development. To bridge the conceptual gap we propose controlled natural language as a textual view on formal specifications in logic. The specification language Attempto Controlled English (ACE) is a subset of natural language that can be accurately and efficiently processed by a computer, but is expressive enough to allow natural usage. The Attempto system translates specifications in ACE into discourse representation structures and into Prolog. The resulting knowledge base can be queried in ACE for verification, and it can be executed for simulation, prototyping and validation of the specification.; Comment: 15 pages, compressed, uuencoded Postscript, to be presented at EMISA Workshop 'Naturlichsprachlicher Entwurf von Informationssystemen - Grundlagen, Methoden, Werkzeuge, Anwendungen', May 28-30, 1996, Ev. Akademie Tutzing

In this paper we present our work in progress towards a domain-specific language called Robot Perception Specification Language (RPSL). RSPL provide means to specify the expected result (task knowledge) of a Robot Perception Architecture in a declarative and framework-independent manner.; Comment: Presented at DSLRob 2013 (arXiv:cs/1312.5952)

Buffering architectures and policies for their efficient management constitute one of the core ingredients of a network architecture. In this work we introduce a new specification language, BASEL, that allows to express virtual buffering architectures and management policies representing a variety of economic models. BASEL does not require the user to implement policies in a high-level language; rather, the entire buffering architecture and its policy are reduced to several comparators and simple functions. We show examples of buffering architectures in BASEL and demonstrate empirically the impact of various settings on performance.; Comment: 11 pages, 11 figures, 2 tables

The primary thesis objective is research into current approaches to design specification languages, emphasizing Ada. Requirements specification is touched upon. Design specification is explored and related to requirements and implementation. The role of language in design is discussed, as well as objectives of the design specification and features that a specification language should provide in order to meet those objectives. Formal language is contrasted with natural language. Some formal specification languages are described, both Ada related and not Ada related. The secondary objective, the thesis project, is to illustrate a design specification in a formal language, Ada. The purpose of the project is to compare the Ada expression of an example design with the natural language specification for the same system.

This project is an application software system providing a graphical interface to PAISLey. PAlSLey (Process Oriented. Applicative. Interpretable Specification Language) is an executable specification language developed at AT&T Bell Labs to model real-time systems. The interface provides the user with a tool to graphically depict a real-time system. The graphics package, called PyGraph, has been implemented on a Sun 3 in a multi-window environment. While developing a graphic, PyGraph generates a PAISLey specification template for the graphic image. The template is filled out by the user with assistance provided by PyGraph.