A hybrid system approach for supporting digital libraries

A digital library (DL) consists of a database which contains library information and a user interface which provides a visual window for users to search relevant information stored in the database. Thus, an abstract structure of a digital library can be defined as a combination of a special purpose database and a user-friendly interface. This paper addresses one of the fundamental aspects of such a combination. This is the formal data structure for linking an object oriented database with hypermedia to support digital libraries. It is important to establish a formal structure for a digital library in order to efficiently maintain different types of library information. This article discusses how to build an object oriented hybrid system to support digital libraries. In particular, we focus on the discussion of a general purpose data model for digital libraries and the design of the corresponding hypermedia interface. The significant features of this research are, first, a formalized data model to define a digital library system structure; second, a practical approach to manage the global schema of a library system; and finally, a design strategy to integrate hypermedia with databases to support a wide range of application areas. Received: 15 December 1997 / Revised: June 1999     

Automatically Detecting and Visualising Errors in UML Diagrams

UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling and analysis of UML diagrams for an automotive industrial case study. Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email: chengb@cse.msu.edu     

Local model checking and protocol analysis

This paper describes a local model-checking algorithm for the alternation-free fragment of the modal mu-calculus that has been implemented in the Concurrency Factory and discusses its application to the analysis of a real-time communications protocol. The protocol considered is RETHER, a software-based, real-time Ethernet protocol developed at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity Ethernet hardware. Our model-checking results show that (for a particular network configuration) RETHER makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller than the total amount that would result from a global analysis of the protocol. In the course of specifying and verifying RETHER, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design also possesses the properties of interest. This observation points out one of the often-overlooked benefits of formal verification: by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to uncover interesting design alternatives.     

High-automation proofs for properties of requirements models

We describe an approach and experimental results in the application of mechanized theorem proving to software requirements analysis. Serving as the test article was the embedded controller for SAFER, a backpack propulsion system used as a rescue device by NASA astronauts. SAFER requirements were previously formalized using the prototype verification system (PVS) during a NASA pilot project in formal methods, details of which appear in a NASA guidebook. This paper focuses on the formulation and proof of properties for the SAFER requirements model. To test the prospects for deductive requirements analysis, we used the PVS theorem prover to explore the upper limits of proof automation. A set of property classes was identified, with matching proof schemes later devised. After developing several PVS proof strategies (essentially prover macros), we obtained fully automatic proofs of 42 model properties. These results demonstrate how customized prover strategies can be used to automate moderate-complexity theorem proving for state machine models.     

Cache consistency by design

Summary. In this paper we present a proof of the sequential consistency of the lazy caching protocol of Afek, Brown, and Merritt. The proof will follow a strategy of stepwise refinement, developing the distributed caching memory in five transformation steps from a specification of the serial memory, whilst preserving the sequential consistency in each step. The proof, in fact, presents a rationalized design of the distributed caching memory. We will carry out our proof using a simple process-algebraic formalism for the specification of the various design stages. We will not follow a strictly algebraic exposition, however. At some points the correctness will be shown using direct semantic arguments, and we will also employ higher-order constructs like action transducers to relate behaviours. The distribution of the design/proof over five transformation steps provides a good insight into the variations that could have been allowed at each point of the design while still maintaining sequential consistency. The design/proof in fact establishes the correctness of a whole family of related memory architectures. The factorization in smaller steps also allows for a closer analysis of the fairness assumptions about the distributed memory.     

Control and data abstraction: the cornerstones of practical formal verification

In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems – Symbolic Model Checking and Deductive Verification, they are still limited in their ability to handle large systems. It is generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization, which break the task of verifying a large system into several smaller tasks of verifying simpler systems. In this paper, we review the two main tools of compositionality and abstraction in the framework of linear temporal logic. We illustrate the application of these two methods for the reduction of an infinite-state system into a finite-state system that can then be verified using model checking. The technical contributions contained in this paper are a full formulation of abstraction when applied to a system with both weak and strong fairness requirements and to a general temporal formula, and a presentation of a compositional framework for shared variables and its application for forming network invariants.     

Using Reason’s Model of Organisational Accidents in Formalising Accident Reports

This paper proposes a method for analysing what are called organisational accidents. The first step of the method involves using Reason’s model of organisational failures. This provides heuristic guidance in identifying both the active and latent conditions that lead to major failures. The second step involves applying formal methods to support a detailed analysis of each latent and active condition. The method is demonstrated on a case study: the railway accident at Watford Junction in the United Kingdom. Analysis of the formal model helps to identify organisational factors that might have prevented the accident. It also helps to identify weaknesses in the report itself. In particular we argue that a signalling standard was misunderstood, the consequences of which could lead to another serious accident.     

Specifying and Analysing System-Level Inter-Component Interfaces

In control systems, the interfaces between software and its embedding environment are a major source of costly errors. For example, Lutz reported that 20–35% of the safety-related errors discovered during integration and system testing of two spacecraft were related to the interfaces between the software and the embedding hardware. Also, the software’s operating environment is likely to change over time, further complicating the issues related to system-level inter-component communication. In this paper we discuss a formal approach to the specification and analysis of inter-component communication using a revised version of RSML (Requirements State Machine Language). The formalism allows rigorous specification of the physical aspects of the inter-component communication and forces encapsulation of communication-related properties in well-defined and easy-to-read interface specifications. This enables us both to analyse a system design to detect incompatibilities between connected components and to use the interface specifications as safety kernels to enforce safety constraints.     

Human Factors in the Design of Supervisory Control Systems and Human–Machine Interfaces for Highly Automated Complex Systems

The design of control systems and human–machine interfaces in the field of complex and safety-critical environments remains today an open issue, in spite of the high technological evolution of the last decades. The increasing use of automation has improved efficiency, safety and ease of operations but, at the same time, it has complicated operators’ situation awareness and has changed the nature of their possible errors. The research activity described in this paper is an attempt to develop a methodological framework to support designers of control systems and human–machine interfaces. In particular, it focuses on the need for a deeply recursive approach related to the implementation of the systemic and human aspects of the design process of a human–machine system, intended as a Joint Cognitive System. A validating case study has been performed, based on the full application of the framework on the control of the turbine/alternator system of a thermoelectric power plant in northern Italy. Correspondence and offprint requests to: M. Piccini, Politecnico di Torino Dipartimento di Energetica, C.so Duca degli Abruzzi 24, 10129 Turin, Italy. Tel.: +39 011 564 4413; Fax: +39 011 564 4499; Email: mipiccin@polito.it     

Verification and optimization of a PLC control schedule

We report on the use of model checking techniques for both the verification of a process control program and the derivation of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure . To compare and interpret the results we carried out the same case study with the aid of the real-time model checker Uppaal, enhanced with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design of the controller and/or derive (time-)optimal schedules within reasonable time and space requirements. Published online: 2 October 2002 The work reported here was carried out while the second and third authors were employed by the Computer Science Department of the University of Nijmegen, Netherlands. The second author was supported by an NWO postdoc grant, the third author by an NWO PhD grant, and both were supported by the EU LTR project VHS (Project No. 26270).     

Comparison of SPIN and VIS for protocol verification

In this paper, we compare and contrast SPIN and VIS, two widely used formal verification tools. In particular, we devote special attention to the efficiency of these tools for the verification of communications protocols that can be implemented either in software or hardware. As a basis of our comparison, we formally describe and verify the Asynchronous Transfer Mode Ring (ATMR) medium access protocol using SPIN and its hardware model using VIS. We believe that this study is of particular interest as more and more protocols, like ATM protocols, are implemented in hardware to match high-speed requirements. Published online: 1 March 2002     

A workshop on formal methods education: held at Melbourne Florida in March 1998[5]

The 21st Century Engineering Consortium Workshop was devoted to educational issues in the area of formal methods. This article summarizes opinions and perspectives which emerged at the workshop and sketches a context for their assessment. There was broad agreement that advances in education are crucial to expanding formal methods practice. However, specific recommendations vary among interest groups and individuals. In this multi-faceted area, it is important to establish a framework for debating issues and presenting them to the broader community. Nowhere is this need greater than in discussions of education.     

Proof engineering in the large: formal verification of Pentium®4 floating-point divider

We examine the challenges presented by large-scale formal verification of industrial-size circuits, based on our experiences in verifying the class of all micro-operations executing on the floating-point division and square root unit of the Intel IA-32 Pentium?4 microprocessor. The verification methodology is based on combining human-guided mechanised theorem-proving with low-level steps verified by fully automated model-checking. A key observation in the work is the need to explicitly address the issues of proof design and proof engineering, i.e., the process of creating proofs and the craft of structuring and formulating them, as concerns on their own right. Published online: 19 November 2002     

A reference framework for continuous interaction

The latest developments in human computer interfaces aim at greater ease of use, and the exploitation of human communication and interaction skills typical of non-computerised environments. This kind of interaction is continuous rather than purely discrete. Continuous interaction implies a tighter coupling between system and user, and raises complicated synchronisation issues where real-time requirements and intrinsic variation of human behaviour play an essential role. In this paper, we propose a human centred layered reference model to reduce the design complexity of systems exhibiting continuous interaction. In the context of the layered model, we discuss the role that formal modelling can play in the design of these systems. Published online: 14 May 2002     

Display Design of Process Systems Based on Functional Modelling

The prevalent way to present information in industrial computer displays is by using piping and instrumentation diagrams. Such interfaces have sometimes resulted in difficulties for operators because they are not sufficient to fulfil their needs. A systematic way that supports interface design therefore has to be considered. In the new design framework, two questions must be answered. Firstly, a modelling method is required to describe a process system. Such a modelling method can define the information content that must be displayed in interfaces. Secondly, how to communicate this information to operators efficiently must be considered. This will provide a basis for determining the visual forms that the information should take. This study discusses interface design of human–machine systems from these two points of view. Based on other scholars’ work, a comprehensive set of functional primitives is summarised as a basis to build a functional model of process systems. A library of geometrical presentations for these primitives is then developed. To support effective interface design, the concept of ‘functional macro’ is introduced and a way to map functional model to interface display is illustrated by applying several principles. To make our ideas clear, a central heating system is taken as an example and its functional model is constructed. Based on the functional model, the information to be displayed is determined. Several functional macros are then found in the model and their corresponding displays are constructed. Finally, by using the library of geometrical presentations for functional primitives and functional macros, the display hierarchy of the central heating system is developed. Reusability of functional primitives makes it possible to use the methodology to support interface design of different process systems.     

The PROSPER toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they can be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the software toolkit developed by the project. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit. Published online: 19 November 2002 Work funded by ESPRIT Framework IV Grant LTR 26241. RID="*" ID="*"Michael Norrish is supported by the Michael and Morven Heller Research Fellowship at St. Catharine’s College, Cambridge. RID="**" ID="**"Konrad Slind is now at the School of Computing, University of Utah, Salt Lake City UT 84112, USA.     

The “Authoring on the Fly” system for automated recording and replay of (tele)presentations

We discuss the problem of capturing media streams which occur during a live lecture in class or during a telepresentation. Instead of presenting yet another method or system for capturing the classroom experience, we introduce some informal guidelines and show their importance for such a system. We derive from these guidelines a formal framework for sets of data streams and an application model to handle these sets so that a real-time replay becomes possible. The Authoring on the Fly system is a possible realization of a framework which follows these guidelines. It allows the capture and real-time replay of data streams captured during a (tele)presentation, including audio, video, and whiteboard action streams. This article gives an overview of the different AoF system components for the various phases of the teaching and learning cycle. It comprises an integrated text and graphics editor for the preparation of pages to be loaded by the whiteboard during the presentation phase. The recording component of the system captures various data streams of the live presentation. They are postprocessed by the system so that they become instances of the class of media for whose replay the general application model was developed. From a global point of view, the Authoring on the Fly system allows one to merge three apparently distinct tasks – teaching in class, telepresentation, and multimedia authoring – into one single activity. The system has been used routinely for recording telepresentations over the MBone net and has already led to a large number of multimedia documents which have been integrated automatically into Web-based teaching and learning environments.     

Attributed point matching for automatic groundtruth generation

Geometric groundtruth at the character, word, and line levels is crucial for designing and evaluating optical character recognition (OCR) algorithms. Kanungo and Haralick proposed a closed-loop methodology for generating geometric groundtruth for rescanned document images. The procedure assumed that the original image and the corresponding groundtruth were available. It automatically registered the original image to the rescanned one using four corner points and then transformed the original groundtruth using the estimated registration transformation. In this paper, we present an attributed branch-and-bound algorithm for establishing the point correspondence that uses all the data points. We group the original feature points into blobs and use corners of blobs for matching. The Euclidean distance between character centroids is used as the error metric. We conducted experiments on synthetic point sets with varying layout complexity to characterize the performance of two matching algorithms. We also report results on experiments conducted using the University of Washington dataset. Finally, we show examples of application of this methodology for generating groundtruth for microfilmed and FAXed versions of the University of Washington dataset documents. Received: July 24, 2001 / Accepted: May 20, 2002