Functional analysis of a real-time protocol for networked control systems

Traditional real-time control systems are tightly integrated into the industrial processes they govern. Now, however, there is increasing interest in networked control systems. These provide greater flexibility and cost savings by allowing real-time controllers to interact with industrial processes over existing communications networks. New data packet queuing protocols are currently being developed to enable precise real-time control over a network with variable propagation delays. We show how one such protocol was formally modelled using timed automata, and how model checking was used to reveal subtle aspects of the control system's dynamic behaviour.

Validation of multicriteria analysis models

Validation procedures play an important role in establishing the credibility of models, improving their relevance and acceptability. This article reviews the testing of models relevant to environmental and natural resource management with particular emphasis on models used in multicriteria analysis (MCA). Validation efforts for a model used in a MCA catchment management study in North Queensland, Australia, are presented. Determination of face validity is found to be a useful approach in evaluating this model, and sensitivity analysis is useful in checking the stability of the model. (C) 2000 Elsevier Science Ltd. All rights reserved.

A formal object-oriented approach to defining consistency constraints for UML models

We discuss how integrity consistency constraints between different UML models can be precisely defined at a language level. In doing so, we introduce a formal object-oriented metamodeling approach. In the approach, integrity consistency constraints between UML models are defined in terms of invariants of the UML model elements used to define the models at the language-level. Adopting a formal approach, constraints are formally defined using Object-Z. We demonstrate how integrity consistency constraints for UML models can be precisely defined at the language-level and once completed, the formal description of the consistency constraints will be a precise reference of checking consistency of UML models as well as for tool development.

Formalising behaviour trees with CSP

Behaviour Trees is a novel approach for requirements engineering. It advocates a graphical tree notation that is easy to use and to understand. Individual requirements axe modelled as single trees which later on are integrated into a model of the system as a whole. We develop a formal semantics for a subset of Behaviour Trees using CSP. This work, on one hand, provides tool support for Behaviour Trees. On the other hand, it builds a front-end to a subset of the CSP notation and gives CSP users a new modelling strategy which is well suited to the challenges of requirements engineering.

A rigorous foundation for pattern based design models

This paper presents a way to describe design patterns rigorously based on role concepts. Rigorous pattern descriptions are a key aspect for patterns to be used as rules for model evolution in the MDA context, for example. We formalize the role concepts commonly used in defining design patterns as a role metamodel using Object-Z. Given this role metamodel, individual design patterns are specified generically as a formal pattern role model using Object-Z. We also formalize the properties that must be captured in a class model when a design pattern is deployed. These properties are defined generically in terms of role bindings from a pattern role model to a class model. Our work provides a precise but abstract approach for pattern definition and also provides a precise basis for checking the validity of pattern usage in designs.

An automated failure mode and effect analysis based on high-level design specificication with behavior trees

Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.

Verifying abstract information flow properties in fault tolerant security devices

The verification of information flow properties of security devices is difficult because it involves the analysis of schematic diagrams, artwork, embedded software, etc. In addition, a typical security device has many modes, partial information flow, and needs to be fault tolerant. We propose a new approach to the verification of such devices based upon checking abstract information flow properties expressed as graphs. This approach has been implemented in software, and successfully used to find possible paths of information flow through security devices.

The real-time refinement calculus: A foundation for machine-independent real-time programming

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a precondition plus post-condition style of specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs may be nonterminating, a further extension is to allow nonterminating repetitions. A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet the specified time; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra's terminology). When such a realtime program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by the specified time. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

Formal verification of ASM designs using the MDG tool

In this paper, we present a formal hardware verification framework linking ASM with MDG. ASM (Abstract State Machine) is a state based language for describing transition systems. MDG (Multiway Decision Graphs) provides symbolic representation of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications, then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We support this work with a case study of an Island Tunnel Controller, which behavior and structure were specified in ASM then using our ASM-MDG tool successfully verified within the MDG tool.

Interfacing ASM with the MDG tool

In this paper we describe an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal verification of ASM descriptions. ASM is a specification method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and axe used primarily for modeling hardware systems. The notions of ASM and MDG axe hence closely related to each other, making it appealing to link these two concepts. The proposed interface between ASM and MDG uses two steps: first, the ASM model is transformed into a flat, simple transition system as an intermediate model. Second, this intermediate model is transformed into the syntax of the input language of the MDG tool, MDG-HDL. We have successfully applied this transformation scheme on a case study, the Island Tunnel Controller, where we automatically generated the corresponding MDG-HDL models from ASM specifications.

Supporting the software testing process through specification animation

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.

Integrating runtime assertions with dynamic types: Structuring a derivation from an incomputable specification

An inherent incomputability in the specification of a functional language extension that combines assertions with dynamic type checking is isolated in an explicit derivation from mathematical specifications. The combination of types and assertions (into "dynamic assertion-types" - DATs) is a significant issue since, because the two are congruent means for program correctness, benefit arises from their better integration in contrast to the harm resulting from their unnecessary separation. However, projecting the "set membership" view of assertion-checking into dynamic types results in some incomputable combinations. Refinement of the specification of DAT checking into an implementation by rigorous application of mathematical identities becomes feasible through the addition of a "best-approximate" pseudo-equality that isolates the incomputable component of the specification. This formal treatment leads to an improved, more maintainable outcome with further development potential.

Proceedings Ninth Asia-Pacific Software Engineering Conference. ASPEC 2002

The following topics are dealt with: Requirements engineering; components; design; formal specification analysis; education; model checking; human computer interaction; software design and architecture; formal methods and components; software maintenance; software process; formal methods and design; server-based applications; review and testing; measurement; documentation; management and knowledge-based approaches.

COMUNICAÇÃO COMUNITÁRIA E PARTICIPAÇÃO POPULAR NO PROJETO CASA BRASIL

Estudo sobre o Projeto Casa Brasil no seu conjunto verificando suas origens e panorama atual, além de enfatizar as experiências de Comunicação Comunitária presentes na unidade Casa Brasil Imbariê. A pesquisa tem como objetivo geral resgatar o contexto histórico do Projeto Casa Brasil e sua situação atual como política pública e sua relação com a Comunicação Comunitária. Por meio de pesquisa bibliográfica constitui-se toda uma base teórica, principalmente no que se refere a Comunicação Comunitária como potencializadora do poder de comunicar. O método utilizado foi o cartográfico, viabilizado por meio das seguintes técnicas: pesquisa documental, entrevistas semiestruturadas e a observação participante. Conclui-se que a Comunicação Comunitária estava prevista nas diretrizes do Projeto Casa Brasil, porém como conceito e prática é uma categoria ausente na maioria das unidades, pois os interesses privados e político-partidários sobrepõem-se ao interesse público, o que aparenta ser um problema estrutural no próprio projeto. Mas, apesar da Casa Brasil Imbariê não se apropriar da Comunicação Comunitária como conceito, se apropria dela na prática, pois as experiências desenvolvidas pelos seus usuários servem como um instrumento de participação popular no exercício da cidadania e promove, em partes, a articulação da comunidade.

A CONSTRUÇÃO DISCURSIVA E A RECEPÇÃO DA HOMOAFETIVIDADE NA TELEDRAMATURGIA BRASILEIRA: consumo, representação e identidade homossexual

Este estudo tem como objetivo avaliar a representação e discurso dos personagens homossexuais da teledramaturgia brasileira e sua potencial relação com as demandas da comunidade homossexual na sua luta por maior tolerância e emancipação. A metodologia inclui dois enfoques analíticos: o primeiro centra-se no campo da produção, a partir dos pressupostos da Análise do Discurso e dos Estudos Queer, verificando os aspectos textuais do discurso e da representação dos personagens gays das telenovelas. O segundo enfoque centra-se no campo da circulação e consumo, mediante os pressupostos dos Estudos de Recepção, a fim de avaliar como os receptores realizam a apropriação do discurso e representação homossexual da telenovela. Esse segundo enfoque conta com um instrumento quantitativo e uma entrevista qualitativa semidirigida, aplicados a uma amostra de 402 participantes, hétero e homossexuais, a maioria jovens estudantes de graduação em Belo Horizonte, MG. Quanto às análises discursivas, os resultados demonstram uma mudança no padrão de representação dos personagens homossexuais, deslocando-se do padrão heteronormativo para uma representação mais humanizada, seguindo o momento histórico de maturidade política da sociedade e a aprovação de marcos legais favoráveis aos sujeitos homossexuais. Quanto aos estudos de recepção, os resultados confirmam o potencial pedagógico da telenovela em ampliar a discussão sobre a questão homoafetiva; auxiliar o sujeito homossexual em aceitar sua identidade sexual e encorajá-lo a assumir sua orientação sexual.