Specifying a safety-critical control system in Z

The paper presents a formal specification in the Z notation for a safety-critical control system. It describes a particular medical device but is quite generic and should be widely applicable. The specification emphasizes safety interlocking and other discontinuous features that are not considered in classical control theory. A method for calculating interlock conditions for particular operations from system safety assertions is proposed; it is similar to ordinary Z precondition calculation, but usually results in stronger preconditions. The specification is presented as a partially complete framework that can be edited and filled in with the specific features of a particular control system. Our system is large but the specification is concise. It is built up from components, subsystems, conditions and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The specification illustrates several useful idioms of the Z notation, and demonstrates that an object-oriented specification style can be expressed in ordinary Z     

网络实时系统的一种活动性描述语言*

介绍了ADL,它是一种基于网络实时系统的活动性描述语言,一种描述并发处理中时态和功能行为的新的形式规格说明符号.ADL专用于计算机网络,是DORIS的一种形式语言扩充.它组合了状态机活动(ASM)的图形符号和基于模型的活动功能行为(AFB)符号;提供了关于ASM的抽象语法和静态、动态语义.最后通过一个小实例说明该语言是如何解释指定网络实时系统的.     

X: Why Z?

Window management systems are now used extensively for user interfaces to computer systems. In particular, X11 has come to dominate the workstation market as a widely accepted industry standard on many different hardware platforms. However, no formal standard currently exists for this window system, both in terms of an international standards body (although this is being addressed), and in terms of a precise (mathematical) specification of what the interface is intended to do. This paper advocates the use of a formal notation to describe such an important system to avoid ambiguity and undesired or unintended variations between different implementations of the same system. Theformal notation used for demonstration purposes, Z, is based on set theory, and has been developed at the Programming Research Group in Oxford.     

POSIX file store in Z/Eves: An experiment in the verified software repository

We present results from the second pilot project in the international Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project’s overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan and Sufrin’s specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories, proof techniques, and experiments reusable across different domains.     

Coding of chemical structures based on a line notation

An algorithm for coding of chemical structures is proposed based on a chemistry oriented line notation language. The latter is based on simple rules providing an almost convention free specification of molecular connectivity. A very useful feature of the proposed molecular code is that it has a line notation form, i.e. it can be interpreted according to the line notation language rules. Both the line notation language and molecular code are based on the principle of decomposition of the molecular graph into biconnected components (cyclic fragments or single atoms). The decomposition graph is a tree, each vertex of which stands for a biconnected component. Within the coding algorithm first the codes for each biconnected component are formed and then they are used as vertex labels of the decomposition tree. Since large chemical graphs usually consist of several biconnected components this method improves, to a great extent, the average time complexity of the algorithm. Terminal cyclic radicals and chain fragments of the molecular graph appear as unique substrings in the line notation code which enhances their computer perception.     

Program Synthesis from Formal Requirements Specifications Using APTS

Formal specifications of software systems are extremely useful because they can be rigorously analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. To transfer this confidence to the actual source code implementation, a formal link is needed between the specification and the implementation. Generating the implementation directly from the specification provides one such link. A program transformation system such as Paige's APTS can be useful in developing a source code generator. This paper describes a case study in which APTS was used to produce code generators that construct C source code from a requirements specification in the SCR (Software Cost Reduction) tabular notation. In the study, two different code generation strategies were explored. The first strategy uses rewrite rules to transform the parse tree of an SCR specification into a parse tree for the corresponding C code. The second strategy associates a relation with each node of the specification parse tree. Each member of this relation acts as an attribute, holding the C code corresponding to the tree at the associated node; the root of the tree has the entire C program as its member of the relation. This paper describes the two code generators supported by APTS, how each was used to synthesize code for two example SCR requirements specifications, and what was learned about APTS from these implementations.