On the Evaluation of a DSL for Architectural Consistency Checking

Software architecture erodes over time and needs to be constantly monitored to be kept consistent with its original intended design. Consistency is rarely monitored using automated techniques. The cost associated to such an activity is typically not considered proportional to its benefits. To improve this situation, we propose Dicto, a uniform DSL for specifying architectural invariants. This language is designed to reduce the cost of consistency checking by offering a framework in which existing validation tools can be matched to newly-defined language constructs. In this paper we discuss how such a DSL can be qualitatively and qualitatively evaluated in practice.

Public acceptability of highway safety countermeasures. Volume II: safe driving conformance research. Final report.

National Highway Traffic Safety Administration, Washington, D.C.

An algorithm for delay checking computer designs.

"Supported in part by the Advanced Research Projects Agency ... under Contract no. US AF 30(602) 4144."

Design of totally self-checking asynchronous sequential machines.

Thesis (M.Sc.)--University of Illinois at Urbana-Champaign.

Checking the correctness of water analyses with freezing point depressions,

Bibliography: leaf 54.

Checking the net contents of packaged goods.

"This fourth supplement was prepared to inform users of changes to NIST Handbook 133 that were adopted at the 79th Annual Meeting of the NCWM ..."

Checking the net contents of packaged goods /

"January 2002."

Rewinding and connecting alternating-current motors; fundamental principles involved in applying and checking lap and wave windings in alternating-current-motor stators and rotors together with practical winding procedure and extensive reference data in typical examples completely worked out, in winding diagrams and in 71 special tabulations, for everyday use by maintenance men in industrial plants, by winders in electrical service and repair shops and by students pursuing electrical courses,

Mode of access: Internet.

Model checking Z specifications using SAL

The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.

Formal analysis of human-computer interaction using model checking

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.