Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Petri net model decomposition - a model based approach supporting distributed execution

Dissertação apresentada para obtenção do Grau de Doutor em Engenharia Electrotécnica, Especialidade de Sistemas Digitais, pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Toimintajärjestelmän hallintaohjelmiston suunnittelu ja toteutus yritysverkostojen käyttöön

Tässä diplomityössä kuvataan sähköisen toimintajärjestelmän hallintaohjelmiston toteuttaminen yritysverkostojen käyttöön. Jokainen toimintajärjestelmän osa on kuvattu erikseen ja sitä vastaamaan on toteutettu oma osio, joka vastaa nykyisten standardien ja spesifikaatioiden vaatimuksiin. Tämän työn standardit ja spesifikaatiot ovat ISO 9001:2000 (laatustandardi), ISO 14001 (ympäristöstandardi) ja OHSAS 18001 (turvallisuusjärjestelmäspesifikaatio). Hallintaohjelmistolla pystytään ylläpitämään toimintajärjestelmän perusosat, joita ovat prosessikuvaukset, asiakirjat, raportit ja mittarit. Ohjelma toteutetaan servlet-tekniikalla web-ympäristöön. Tietokantaratkaisuna käytetään SQL:ää, joka sopii hyvin yhteen Javan kanssa. Käyttöliittymänä on selain, mikä osaltaan helpottaa käyttöönottoa yrityksissä, koska erillisiä asennuksia käyttäjien koneisiin ei tarvita. Ohjelma on tarkoitettu asennettavaksi yrityksen sisäverkkoon.

Ympäristöjärjestelmän ja työterveys- ja työturvallisuusjohtamisjärjestelmän rakentaminen ja liittäminen laadunhallintajärjestelmään

Työ toteutettiin satamaoperaattori Steveco Oy:ssä. Työn lähtökohtana oli Stevecon tarve kehittää laadunhallintajärjestelmän pohjalle toimintajärjestelmä, johon sisältyy laadunhallintajärjestelmän lisäksi ympäristöjärjestelmä ja työterveys- ja työturvallisuusjohtamisjärjestelmä. Työssä pohdittiin käytäntöjä kolmen järjestelmän yhdistämiseksi. Toimintajärjestelmä rakentui olemassa olevan laatujärjestelmän pohjalle siten, että laatujärjestelmän elementtejä, muun muassa laatukäsikirjaa, hyödynnettiin toimintajärjestelmässä, ja lisäksi ympäristö- ja työterveys- ja työturvallisuusjärjestelmiin liittyviä laatujärjestelmästä erillisiä toimintajärjestelmän osia yhdistettiin. Ympäristöjärjestelmän pohjana käytettiin ISO/DIS 14001:2003 ympäristöjärjestelmästandardiehdotusta ja työterveys- ja työturvallisuusjohtamisjärjestelmän pohjana OHSAS 18001:fi:2003 turvallisuusjärjestelmä spesifikaatiota. Erillisiä ympäristöjärjestelmän osia toimintajärjestelmässä ovat ympäristönäkökohtien kartoitus ja merkittävyyden arviointi sekä ympäristöpäämäärät ja tavoitteet. Erillisiä työterveys- ja työturvallisuusjohtamisjärjestelmässä toteutettavia osia ovat riskien arviointi ja työterveys- ja työturvallisuuspäämäärät.

Lappeenrannan ulkovalaistusverkon verkkotietojärjestelmän modernisointi

Sähköisen verkon täsmällinen tunteminen on edellytys verkon tehokkaalle suunnittelulle ja käytölle. Lappeenrannassa ulkovalaistusverkon dokumentointi oli lähtökohtaisestei hyvin hajanaista. Tämän tutkimuksen tärkein anti oli tarjota Lappeenrannan kaupungille dokumentointiratkaisu, jolla ulkovalaistusverkon dokumentaatio ja topologia saatetaan moderniin sähköiseen muotoon. Tutkimus jakaantui neljään eri pääkohtaan: Lappeenrannan ulkovalaistusverkon tutkimustyöhön, verkkotietojärjestelmien tutkimustyöhön, dokumentointiprosessin määrittelyyn ja verkkotietojärjestelmien ylläpitoprosessin määrittelyyn. Näissä on käytetty merkittävissä määrin asiantuntijoiden lausuntoja, erityisesti ulkovalaistusverkon rakenteesta ja eri verkkotietojärjestelmien ominaisuuksista sekä käytöstä. Näihin perustuen on muodostettu kuva uuden verkkotietojärjestelmän vaatimuksista ja dokumentoinnin lähtötasosta, joiden avulla on määritelty itse dokumentointiprosessi, sen potentiaaliset ongelmat ja arvioitu työmäärää. Ylläpitoprosessien määrittelyssä on käytetty lähtökohtana Lappeenrannan Energiaverkot Oy:n nykyisiä ylläpitoprosesseja ja -menetelmiä. Tutkimuksen tuloksena syntyi määrittelyt kolmelle eri verkkotietojärjestelmälle, joilla ongelma saadaan ratkaistua. Näistä kaksi täytti vaatimukset täysin: Trimble NIS ja Keypron KeyLight.

Timing verification in transaction modeling

Les systèmes Matériels/Logiciels deviennent indispensables dans tous les aspects de la vie quotidienne. La présence croissante de ces systèmes dans les différents produits et services incite à trouver des méthodes pour les développer efficacement. Mais une conception efficace de ces systèmes est limitée par plusieurs facteurs, certains d'entre eux sont: la complexité croissante des applications, une augmentation de la densité d'intégration, la nature hétérogène des produits et services, la diminution de temps d’accès au marché. Une modélisation transactionnelle (TLM) est considérée comme un paradigme prometteur permettant de gérer la complexité de conception et fournissant des moyens d’exploration et de validation d'alternatives de conception à des niveaux d’abstraction élevés. Cette recherche propose une méthodologie d’expression de temps dans TLM basée sur une analyse de contraintes temporelles. Nous proposons d'utiliser une combinaison de deux paradigmes de développement pour accélérer la conception: le TLM d'une part et une méthodologie d’expression de temps entre différentes transactions d’autre part. Cette synergie nous permet de combiner dans un seul environnement des méthodes de simulation performantes et des méthodes analytiques formelles. Nous avons proposé un nouvel algorithme de vérification temporelle basé sur la procédure de linéarisation des contraintes de type min/max et une technique d'optimisation afin d'améliorer l'efficacité de l'algorithme. Nous avons complété la description mathématique de tous les types de contraintes présentées dans la littérature. Nous avons développé des méthodes d'exploration et raffinement de système de communication qui nous a permis d'utiliser les algorithmes de vérification temporelle à différents niveaux TLM. Comme il existe plusieurs définitions du TLM, dans le cadre de notre recherche, nous avons défini une méthodologie de spécification et simulation pour des systèmes Matériel/Logiciel basée sur le paradigme de TLM. Dans cette méthodologie plusieurs concepts de modélisation peuvent être considérés séparément. Basée sur l'utilisation des technologies modernes de génie logiciel telles que XML, XSLT, XSD, la programmation orientée objet et plusieurs autres fournies par l’environnement .Net, la méthodologie proposée présente une approche qui rend possible une réutilisation des modèles intermédiaires afin de faire face à la contrainte de temps d’accès au marché. Elle fournit une approche générale dans la modélisation du système qui sépare les différents aspects de conception tels que des modèles de calculs utilisés pour décrire le système à des niveaux d’abstraction multiples. En conséquence, dans le modèle du système nous pouvons clairement identifier la fonctionnalité du système sans les détails reliés aux plateformes de développement et ceci mènera à améliorer la "portabilité" du modèle d'application.

Design of highly parallel architecture with Alpha and Handel

We propose a bridge between two important parallel programming paradigms: data parallelism and communicating sequential processes (CSP). Data parallel pipelined architectures obtained with the Alpha language can be embedded in a control intensive application expressed in CSP-based Handel formalism. The interface is formally defined from the semantics of the languages Alpha and Handel. This work will ease the design of compute intensive applications on FPGAs.

A compositional framework for hardware/software co-design

We describe a compositional framework, together with its supporting toolset, for hardware/software co-design. Our framework is an integration of a formal approach within a traditional design flow. The formal approach is based on Interval Temporal Logic and its executable subset, Tempura. Refinement is the key element in our framework because it will derive from a single formal specification of the system the software and hardware parts of the implementation, while preserving all properties of the system specification. During refinement simulation is used to choose the appropriate refinement rules, which are applied automatically in the HOL system. The framework is illustrated with two case studies. The work presented is part of a UK collaborative research project between the Software Technology Research Laboratory at the De Montfort University and the Oxford University Computing Laboratory.

From SMART to agent systems development

n order for agent-oriented software engineering to prove effective it must use principled notions of agents and enabling specification and reasoning, while still considering routes to practical implementation. This paper deals with the issue of individual agent specification and construction, departing from the conceptual basis provided by the smart agent framework. smart offers a descriptive specification of an agent architecture but omits consideration of issues relating to construction and control. In response, we introduce two new views to complement smart: a behavioural specification and a structural specification which, together, determine the components that make up an agent, and how they operate. In this way, we move from abstract agent system specification to practical implementation. These three aspects are combined to create an agent construction model, actsmart, which is then used to define the AgentSpeak(L) architecture in order to illustrate the application of actsmart.

Modelagem em SystemC-AMS de uma plataforma compatível com o sistema de coleta de dados brasileiro

This work presents simulation results of an identification platform compatible with the INPE Brazilian Data Collection System, modeled with SystemC-AMS. SystemC-AMS that is a library of C++ classes dedicated to the simulation of heterogeneous systems, offering a powerful resource to describe models in digital, analog and RF domains, as well as mechanical and optic. The designed model was divided in four parts. The first block takes into account the satellite s orbit, necessary to correctly model the propagation channel, including Doppler effect, attenuation and thermal noise. The identification block detects the satellite presence. It is composed by low noise amplifier, band pass filter, power detector and logic comparator. The controller block is responsible for enabling the RF transmitter when the presence of the satellite is detected. The controller was modeled as a Petri net, due to the asynchronous nature of the system. The fourth block is the RF transmitter unit, which performs the modulation of the information in BPSK ±60o. This block is composed by oscillator, mixer, adder and amplifier. The whole system was simulated simultaneously. The results are being used to specify system components and to elaborate testbenchs for design verification

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

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

Geração automática de hardware a partir de especificações formais: estendendo uma abordagem de tradução

Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification

Emergency management in the highways of the future. A performance-based multilayered ITS architecture design proposal

Emergency management is one of the key aspects within the day-to-day operation procedures in a highway. Efficiency in the overall response in case of an incident is paramount in reducing the consequences of any incident. However, the approach of highway operators to the issue of incident management is still usually far from a systematic, standardized way. This paper attempts to address the issue and provide several hints on why this happens, and a proposal on how the situation could be overcome. An introduction to a performance based approach to a general system specification will be described, and then applied to a particular road emergency management task. A real testbed has been implemented to show the validity of the proposed approach. Ad-hoc sensors (one camera and one laser scanner) were efficiently deployed to acquire data, and advanced fusion techniques applied at the processing stage to reach the specific user requirements in terms of functionality, flexibility and accuracy.

Configuración de un entorno de trabajo para el desarrollo de software ágil con integración continua

Hoy en día, existen numerosos sistemas (financieros, fabricación industrial, infraestructura de servicios básicos, etc.) que son dependientes del software. Según la definición de Ingeniería del Software realizada por I. Sommerville, “la Ingeniería del Software es una disciplina de la ingeniería que comprende todos los aspectos de la producción de software desde las etapas iniciales de la especificación del sistema, hasta el mantenimiento de éste después de que se utiliza.” “La ingeniería del software no sólo comprende los procesos técnicos del desarrollo de software, sino también actividades tales como la gestión de proyectos de software y el desarrollo de herramientas, métodos y teorías de apoyo a la producción de software.” Los modelos de proceso de desarrollo software determinan una serie de pautas para poder desarrollar con éxito un proyecto de desarrollo software. Desde que surgieran estos modelos de proceso, se investigado en nuevas maneras de poder gestionar un proyecto y producir software de calidad. En primer lugar surgieron las metodologías pesadas o tradicionales, pero con el avance del tiempo y la tecnología, surgieron unas nuevas llamadas metodologías ágiles. En el marco de las metodologías ágiles cabe destacar una determinada práctica, la integración continua. Esta práctica surgió de la mano de Martin Fowler, con el objetivo de facilitar el trabajo en grupo y automatizar las tareas de integración. La integración continua se basa en la construcción automática de proyectos con una frecuencia alta, promoviendo la detección de errores en un momento temprano para poder dar prioridad a corregir dichos errores. Sin embargo, una de las claves del éxito en el desarrollo de cualquier proyecto software consiste en utilizar un entorno de trabajo que facilite, sistematice y ayude a aplicar un proceso de desarrollo de una forma eficiente. Este Proyecto Fin de Grado (PFG) tiene por objetivo el análisis de distintas herramientas para configurar un entorno de trabajo que permita desarrollar proyectos aplicando metodologías ágiles e integración continua de una forma fácil y eficiente. Una vez analizadas dichas herramientas, se ha propuesto y configurado un entorno de trabajo para su puesta en marcha y uso. Una característica a destacar de este PFG es que las herramientas analizadas comparten una cualidad común y de alto valor, son herramientas open-source. El entorno de trabajo propuesto en este PFG presenta una arquitectura cliente-servidor, dado que la mayoría de proyectos software se desarrollan en equipo, de tal forma que el servidor proporciona a los distintos clientes/desarrolladores acceso al conjunto de herramientas que constituyen el entorno de trabajo. La parte servidora del entorno propuesto proporciona soporte a la integración continua mediante herramientas de control de versiones, de gestión de historias de usuario, de análisis de métricas de software, y de automatización de la construcción de software. La configuración del cliente únicamente requiere de un entorno de desarrollo integrado (IDE) que soporte el lenguaje de programación Java y conexión con el servidor. ABSTRACT Nowadays, numerous systems (financial, industrial production, basic services infrastructure, etc.) depend on software. According to the Software Engineering definition made by I.Sommerville, “Software engineering is an engineering discipline that is concerned with all aspects of software production from the early stages of system specification through to maintaining the system after it has gone into use.” “Software engineering is not just concerned with the technical processes of software development. It also includes activities such as software project management and the development of tools, methods, and theories to support software production.” Software development process models determine a set of guidelines to successfully develop a software development project. Since these process models emerged, new ways of managing a project and producing software with quality have been investigated. First, the so-called heavy or traditional methodologies appeared, but with the time and the technological improvements, new methodologies emerged: the so-called agile methodologies. Agile methodologies promote, among other practices, continuous integration. This practice was coined by Martin Fowler and aims to make teamwork easier as well as automate integration tasks. Nevertheless, one of the keys to success in software projects is to use a framework that facilitates, systematize, and help to deploy a development process in an efficient way. This Final Degree Project (FDP) aims to analyze different tools to configure a framework that enables to develop projects by applying agile methodologies and continuous integration in an easy and efficient way. Once tools are analyzed, a framework has been proposed and configured. One of the main features of this FDP is that the tools under analysis share a common and high-valued characteristic: they are open-source. The proposed framework presents a client-server architecture, as most of the projects are developed by a team. In this way, the server provides access the clients/developers to the tools that comprise the framework. The server provides continuous integration through a set of tools for control management, user stories management, software quality management, and software construction automatization. The client configuration only requires a Java integrated development environment and network connection to the server.

An Exploration of parametric software cost estimating models for Jackson Systems Development

Most parametric software cost estimation models used today evolved in the late 70's and early 80's. At that time, the dominant software development techniques being used were the early 'structured methods'. Since then, several new systems development paradigms and methods have emerged, one being Jackson Systems Development (JSD). As current cost estimating methods do not take account of these developments, their non-universality means they cannot provide adequate estimates of effort and hence cost. In order to address these shortcomings two new estimation methods have been developed for JSD projects. One of these methods JSD-FPA, is a top-down estimating method, based on the existing MKII function point method. The other method, JSD-COCOMO, is a sizing technique which sizes a project, in terms of lines of code, from the process structure diagrams and thus provides an input to the traditional COCOMO method.The JSD-FPA method allows JSD projects in both the real-time and scientific application areas to be costed, as well as the commercial information systems applications to which FPA is usually applied. The method is based upon a three-dimensional view of a system specification as opposed to the largely data-oriented view traditionally used by FPA. The method uses counts of various attributes of a JSD specification to develop a metric which provides an indication of the size of the system to be developed. This size metric is then transformed into an estimate of effort by calculating past project productivity and utilising this figure to predict the effort and hence cost of a future project. The effort estimates produced were validated by comparing them against the effort figures for six actual projects.The JSD-COCOMO method uses counts of the levels in a process structure chart as the input to an empirically derived model which transforms them into an estimate of delivered source code instructions.