Formal Specification of Computer-Based Systems
J.UCS Special Issue

Miroslav Sveda (Brno University of Technology, Czech Republic)
sveda@fit.vutbr.cz

Charles Rattray (University of Stirling, Stirling, UK)
cr@cs.stir.ac.uk

Jerzy Rozenblit (University of Arizona, Tucson, USA)
Jerzy.Rozenblit@arizona.edu

The 5^th Workshop on Formal Specification of Computer-Based Systems (FSCBS) took place in Brno, Czech Republic, in May 2004. This special issue presents a collection of papers from that last Workshop. Previous Workshops were held in Edinburgh, Scotland (2000), Washington, D.C. (2001), Lund, Sweden (2002) and Huntsville, Alabama (2003); a 6^th Workshop, on the same theme, will take place in Washington, D.C., in April 2005, again as part of the annual IEEE International conferences on Engineering of Computer-Based Systems (ECBS), the 12^th such conference. The Co-Chairs, and organisers of these workshops, are Miroslav Sveda (CZ), Charles Rattray (UK), Jerzy Rozenblit (USA). The ever-expanding application of increasingly sophisticated computer-based systems (CBS) in a diversity of fields such as engineering, science, commerce and education, demands better understanding of the scale, complexity and heterogenity in the specification, analysis, design of such systems and highlights the practical need for better formal approaches and better tool development. Formal specification becomes more acute and urgent than ever as we try to deal with the practical problems of today and the future. It is clear that finding common general descriptions of such heterogeneous systems, particularly the use of formal notations to describe assumptions, requirements and design of CBS, is a great challenge that is worth our every effort. The FSCBS Workshops arose out of our modest attempts to deal with such situations.

The last workshop, as in the previous ones, provided a forum for researchers and practitioners from industry in which FSCBS-related discussions focused on completed work and work-in-progress, covering software, hardware and mixed hardware/software applications.

Contributions presented by authors from North America, Europe and Australia have been extended to full papers and after the reviewing process the following five papers have been selected for this special issue of the J.UCS:

The paper "A MOF-Based Metamodeling Environment" by Matthew Emerson, Janos Sztipanovits and Ted Bapty focuses on the use of MOF (Meta Object Facility), one of the core standards of the Model Driven Architecture of the Object Management Group, as a metamodeling language and describes their work on changing their MIC (Model-Integrated Computing) environment from UML/OCL to MOF. On the way, they highlight some of the inadequacies of MOF for their purposes. Their results are illustrated on a lengthy example.

In the paper, "Platform Modeling and Model Transformations for Analysis", Tivadar Szemethy and Gabor Karsai argue that there is a need for modeling the execution platform of embedded systems and show how a knowledge of the platform models could be used to transform embedded system application models into models that could be subjected to formal verification through model checking; such an approach can also provide details about implementing the translation algorithm itself. Illustrative examples show some of the benefits of the approach.

Mark Dent, Andrew Solomon, John Leaney and Tim O'Neill, in their paper "Architectural Abstraction as Transformation of Poset Labelled Graphs", are concerned with the architectural design of large, and possibly complex, computer-based systems. The level of concern is that any model of such system architecture should be reasonably intuitive and accessible to practitioners in industry, and should be scalable. In this respect, they have chosen a model that will deal with the topology, type and levels of abstraction inherent in any architectural design. The model is novel, is based on the application of the category of poset labelled graphs and their transformations, and is illustrated by a number of simple but pertinent examples show levels of design abstraction and transformation. Problems of constraint and coherency in relating the relationships between architectural abstractions and their refinements are indicated. The longer term goal is the development of suitable tools to help the practising designer to deal with such problems.

The paper "Synchronization Can Improve Control and Modularity" by Cristina Seceleanu and Tiberiu Seceleanu is concerned with two important aspects of reactive system design, namely behaviour control and modularity within the framework of action systems. The authors introduce an additional concurrency mechanism (barrier synchronization) as a way to describe controllable behaviour by defining a new parallel composition operator. The effects are amply illustrated by various examples and proofs given in the paper.

The final paper "Tools for Parametric Verification. A Comparison on a Case Study" by Petr Matousek is concerned with protocol analysis involving several parameters such as transmission delay or the length of the transmitting window. The paper reports on the synthesis of parameters of the PGM (Pragmatic General Multicast) protocol - a reliable multicast transport protocol for applications that transfer data from multiple sources to multiple receivers.

Using a formal model based on extended time automata with parameters, verification of the reliability property is considered where this property states that PGM should either receive all data packets from transmissions and repairs, or be able to detect unrecoverable data packets loss. The verification uses a model checking approach and compares the merits of the HYTECH, TREX, UPPAAL tools in the case study.

This is the third special J.UCS issue based on the Formal Specification of Computer-Based Systems Workshops.