The aim of this thesis is to create a tool for formal verification of systems specified using textual use- cases. The tool should allow for automated verification of temporal invariants specified in temporal logic (CTL and LTL formulae). The textual specification is transformed to a formal model that is verified using the NuSMV symbolic model-checker. Potential errors are shown to the user in the form of an HTML report. Using this feedback, the user is able to iteratively develop valid textual use-case specifications. The tool's architecture should be focused on reusability of its components and extensibility. Powered by TCPDF (www.tcpdf.org)

No description available.

<p> With the growth of technology there is recognition of the fact that communication requires improving between decision-makers and the people who will eventually use or be affected by the system under consideration. The main thrust of this work is to explore means of facilitating clear unambiguous communication of relevant needs to all parties involved in the design process.</p> <p> A number of approaches to this problem from different disciplines are reviewed. Some of these approaches are already in existence while others require adapting to the particular problems encountered in the design process.</p> <p> Suggestions are put foreward as to how these techniques can be integrated to produce a unified approach to the problem of producing a Total Specification embodying all information necessary to the designer in his capacity as decision-maker.</p> / Thesis / Master of Engineering (MEngr)

This thesis investigates the properties of generic refinements of behavioral specifications. At the base of this investigation stands the view from algebraic specification that abstract data types can be modeled as algebras. A specification of a data type is formed from a syntactic part, i.e. a signature detailing the interface of the data type, and a semantic part, i.e. a class of algebras (called its models) that contains the valid implementations of that data type. Typically, the class of algebras that constitutes the semantics of a specification is defined as the class of algebras that satisfy some given set of axioms. The behavioral aspect of a specification comes from relaxing the requirements imposed by axioms, i.e. by allowing in the semantics of a specification not only the algebras that literally satisfy the given axioms, but also those algebras that appear to behave according to those axioms. Several frameworks have been developed to express the adequate notions of what it means to be a behavioral model of a set of axioms, and our choice as the setting for this thesis will be Bidoit and Hennicker’s Constructor-based Observational Logic, abbreviated COL. Using specifications that rely on the behavioral aspects defined by COL we study the properties of generic refinements between specifications. Refinement is a relation between specifications. The refinement of a target specification by a source specification is given by a function that constructs models of the target specification from the models of the source specification. These functions are called constructions and the source and target specifications that they relate are called the context of the refinement. The theory of refinements between algebraic specifications, with or without the behavioral aspect, has been well studied in the literature. Our analysis starts from those studies and adapts them to COL, which is a relatively new framework, and for which refinement has been studied only briefly. The main part of this thesis is formed by the analysis of generic refinements. Generic refinements are represented by constructions that can be used in various contexts, not just in the context of their definition. These constructions provide the basis for modular refinements, i.e. one can use a locally defined construction in a global context in order to refine just a part of a source specification. The ability to use a refinement outside its original context imposes additional requirements on the construction that represents it. An implementer writing such a construction must not use details of the source models that can be contradicted by potential global context requirements. This means, roughly speaking, that he must use only the information available in the source signature and also any a priori assumption that was made about the contexts of use. We look at the basic case of generic refinements that are reusable in every global context, and then we treat a couple of variations, i.e. generic refinements for which an a priori assumption it is made about the nature of their usage contexts. In each of these cases we follow the same pattern of investigation. First we characterize the constructions that ensure reusability by means of preservation of relations, and then, in most cases, we show that such constructions must be definable in terms of their source signature. Throughout the thesis we use an informal analogy between generic (i.e. polymorphic) functions that appear in second order lambda calculus and the generic refinements that we are studying. This connection will enable us to describe some properties of generic refinements that correspond to the properties of polymorphic functions inferred from their types and named “theorems for free” by Wadler. The definability results, the connection between the assumptions made about the usage contexts and the characterizing relations, and the “theorems for free” for behavioral specifications constitute the main contributions of this thesis.

Complex software-security policies are dicult to specify, understand, and update. The same is true for complex software in general, but while many tools and techniques exist for decomposing complex general software into simpler reusable modules (packages, classes, functions, aspects, etc.), few tools exist for decomposing complex security policies into simpler reusable modules. The tools that do exist for modularizing policies either encapsulate entire policies as atomic modules that cannot be decomposed or allow ne-grained policy modularization but require expertise to use correctly. This dissertation presents a policy-composition tool called PoliSeer [27, 26] and the PoCo policy-composition software-security language. PoliSeer is a GUI-based tool designed to enable users who are not expert policy engineers to exibly specify, visualize, modify, and enforce complex runtime policies on untrusted software. PoliSeer users rely on expert policy engineers to specify universally composable policy modules; PoliSeer users then build complex policies by composing those expert-written modules. This dissertation describes the design and implementation of PoliSeer and a case study in which we have used PoliSeer to specify and enforce a policy on PoliSeer itself. PoCo is a language for specifying composable software-security policies. PoCo users specify software-security policies in terms of abstract input-output event sequences. The policy outputs are expressive, capable of describing all desired, irrelevant, and prohibited events at once. These descriptive outputs compose well: operations for combining them satisfy a large number of algebraic properties, which allows policy hierarchies to be designed more simply and naturally. We demonstrate PoCo's capability via a case study in which a sophisticated policy is implemented in PoCo.

This work is dedicated to the requierements specification process automation issues. Main goal of the paper is to specify a conceptual model of the multy-user software requirements specification system and create a working prototype of this model. Analysis part of the work focuses on requirement specification templates and existing requirements specification software investigation. A detailed analysis of most popular templates Volere and IEEE STD 830-1998 is followed by existing software requirements specification software analysis : AnalystPRO and RequisitePRO. Requirements and tasks for the system prototype are raised on the basis of main features and weknesses of analysed requirements specification templates and software. This work presents a complete conceptual model of the software requirements specification automation. System model is based on the Volere template. Main features of the system prototype are as follows: complete independence from operating system and working environment, no any client software installation is needed, server part does not require any special components installation and is based on popular free software: Apache and MySQL Servers. System architecture is based on JAVA Applets technology. Working prototype is an implementation of main system protoype features. This is a multy-user software requirements specification environment with all main collaboration fetures: version control, document locking, presence awareness. Usability of system... [to full text]

Darbe pristatomas reikalavimų specifikavimo šablonais modelis. Aptariama aukštos kokybės reikalavimų proceso nauda kuriamoms sistemoms. Pateikiami išanalizuotų reikalavimų specifikacijos dokumento standartų ir reikalavimų inžinerijos programinių įrankių detalios analizės rezultatai. Pristatoma koncepcija geriau užtikrinanti reikalavimų identifikavimo ir specifikavimo kokybę - sumodeliuotas reikalavimų specifikacijos modelis, panaudojantis Volere reikalavimų surinkimo šabloną, pritaikant reikalavimų specifikavimo programinės įrangos įrankį Telelogic Doors. Sukurto prototipo pagalba, sistema automatizuoja reikalavimų surinkimo procesą, sumažindama 30 % vartotojo veiksmų, taip sudarydama didesnį vartotojo darbo našumą ir efektyvumą reikalavimų specifikavimo procese. / The main object of this thesis is to analyze requirements specification templates and requirements management tools and realize model prototype using requirements specification templates. There are analyze of requirements templates and requirements managing tools results in considering about a gain of high quality requirements process. To introduce a conception witch supports clearly requirement specification process – the model of Volere requirements specification template adopting Telelogic Doors requirements managing tool. Model realized in Doors using DXL - Doors eXtension Language. Created prototype reduce 30% of users activities and lets user to get more efficiency and productivity in requirements specification process.

Category theory is proving a useful tool in programming and program specification - not only as a descriptive language but as directly applicable to programming and specification tasks. Category theory achieves a level of generality of description at which computation is still possible. We show that theorems from category theory often have constructive proofs in the sense that they may be encoded as programs. In particular we look at the computation of colimits in categories showing that general theorems give rise to routines which considerably simplify the rather awkward computation of colimits. The general routines arising from categorical constructions can be used to build programs in the 'combinatorial' style of programming. We show this with an example - a program to implement the semantics of a specification language. More importantly, the intimate relationship between these routines and algebraic specifications allows us to develop programs from certain forms of specifications. Later we turn to algebraic specifications themselves and look at properties of "monadic theories". We establish that, under suitable conditions: 1. Signatures and presentations may be defined for monadic theories and free theories on a signature may be constructed. 2. Theory morphisms give rise to ad junctions between categories of algebras and moreover a collection of algebras of a theory give rise to a new theory with certain properties. 3. Finite colimits and certain factorisations exist in categories of monadic theories. 4. Many-sorted, order-sorted and even category-sorted theories may be handled by somewhat extending the notion of monadic theories. These results show that monadic theories are sufficiently well-behaved to be used in the semantics of algebraic specification languages. Some of the constructions can be encoded as programs by the techniques mentioned above.

Machine emulation allows for the simulation of a real or virtual machine, the source machine, on various host computers. A machine emulator interprets programs that are compiled for the emulated machine, but normally at a much reduced speed. Therefore, in order to increase the executions peed of such interpreted programs, a machine emulator may apply different dynamic optimization techniques. In our research we focus on emulators for real machines, i.e. existing computer architectures, and in particular on dynamic binary translation as the optimization technique. With dynamic binary translation, the machine instructions of the interpreted source program are translated in to machine instructions for the host machine during the interpretation of the program. Both, the machine emulator and its dynamic binary translator a resource and host machine specific, respectively, and are therefore traditionally hand-written. In this thesis we introduce the Walkabout/Yirr-Ma framework. Walkabout, initially developed by Sun Micro systems, allows among other things for the generation of instrumented machine emulators from a certain type of machine specification files. We extended Walkabout with our generic dynamic optimization framework ‘Yirr-Ma’ which defines an interface for the implementation of various dynamic optimizers: by instrumenting a Walkabout emulator’s instruction interpretation functions, Yirr-Ma observes and intercepts the interpretation of a source machine program, and applies dynamic optimizations to selected traces of interpreted instructions on demand. One instance of Yirr-Ma’s interface for dynamic optimizers implements our specification-driven dynamic binary translator, the major contribution of this thesis. At first we establish two things: a formal framework that describes the process of machine emulation by abstracting from real machines, and different classes of applicable dynamic optimizations. We define dynamic optimizations by a set of functions over the abstracted machine, and dynamic binary translation as one particular optimization function. Using this formalism, we then derive the upper bound for quality of dynamically translated machine instructions. Yirr-Ma’s dynamic binary translator implements the optimization functions of our formal framework by modules which are either generated from, or parameterized by, machine specification files. They thus allow for the adaptation of the dynamic binary translator to different source and host machines without hand-writing machine dependent code.

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, Orientação a Objetos e Especificação de Processos e Concorrência, em uma Única abordagem expressa através de uma Linguagem de Especificação Formal, chamada LOP. Esta linguagem a de natureza algébrica, com destaque para a semântica baseada em teorias em lógica de primeira ordem e na construção incremental de especificações baseada em bibliotecas. / The abstract specification of data types, one of the most important concepts accepted and understood of the Computer Science, allows to describe the the main entities of a based-computer system through the properties that these entities should be to satisfy. This is made using algebraic methods and languages, where the properties are defined as axioms (equations). By other hand, the technology called Object-Oriented (00), it has been transformed in a mature discipline for Design and Implementations of software applications. At present, this technology include many methodologies and many languages for the totality of the system development process. But the majority are influenced by the implementation of such systems, i.e., the basic concepts 00 of class, object and inheritance are defined in accordance with the programming language to be used. Moreover, we noted that the last years are being developed many research on a computer generation that involve massively parallel architectures (concurrent computing) as well as on data communication systems and protocol engineering (description). The main objective of this thesis is to give an answer to these three subjects integrating three basic concepts of Software Engineering: Algebraic Specification, Object Orientation and Processes and Concurrency specification, in an unique approach expressed through a language of formal specification, called LOP. This language has algebraic nature with prominence to the semantics based on theories in first-order logic with equality and the incremental construction of library-based specifications.