ProcGraph: a procedure-oriented graphical notation for process-control software specification

This paper presents a procedure-centric approach to process-control software specification. A high-level, domain-specific specification notation called ProcGraph was developed, based on three types of diagrams that describe the modelled system using a domain-oriented hierarchical structure of interdependent procedural control entities and state-transition diagrams. The state-transition diagrams describe the behaviour of the procedural control entities. The processing content of the states is defined by sequential programs. In order to illustrate the presented models and notation, some segments of a real process-control application that deals with the drying process in the production of titanium dioxide are presented.     

事务工作流模型定义及完全性分析

事务工作流模型可被视为扩展的事务模型和通用工作流模型的交汇点，提出将工作流的模型定义同其事务属性的定义独立开来，尽管在此方法中区分了多重的事务属性。提出了直观的注解符来定义原子性，提供了一个通用规则——放宽的完全性准则，以适应现实运行中事务管理的需要，以一个网上电子书店工作流应用为例来阐明这种思路。     

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     

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.     

Use case maps as architectural entities for complex systems

The paper presents a novel, scenario based notation called Use Case Maps (UCMs) for describing, in a high level way, how the organizational structure of a complex system and the emergent behavior of the system are intertwined. The notation is not a behavior specification technique in the ordinary sense, but a notation for helping a person to visualize, think about, and explain the big picture. UCMs are presented as “architectural entities” that help a person stand back from the details during all phases of system development. The notation has been thoroughly exercised on systems of industrial scale and complexity and the distilled essence of what has been found to work in practice is summarized. Examples are presented that confront difficult complex system issues directly: decentralized control, concurrency, failure, diversity, elusiveness and fluidity of runtime views of software, self modification of system makeup, difficulty of seeing large scale units of emergent behavior cutting across systems as coherent entities (and of seeing how such entities arise from the collective efforts of components), and large scale     

A framework for neural net specification

A notation for the specification of neural nets is proposed. The aim is to produce a simple mathematical framework for use in specifying neural nets essentially by defining their transfer functions and connections. Nets are specified as interacting processing elements (nodes), communicating via instant links. Dynamics and adaptation are defined at the processing elements themselves, and all interaction is explicitly specified by directed arcs. Specifications can be built up hierarchically by turning a specification into a generator for a node, or they can be developed top-down. The use of the system is illustrated     

一种从Z规约到并行程序的精化方法

提出了一种通过对设计模式进行精化,从Z规约开发并行程序的方法.该方法对Z语言进行了并行扩充,从Z功能规约出发,通过使用扩展的设计模式逐步精化得到并行的设计规约,再通过保持语义的转换,得到可最后转换为并行代码的抽象并行程序.通过实例对这一方法进行了详细的描述.     

The influence of formal representation on solution specification

The effectiveness and value of a notation is determined by how well its users are able to work with it. This paper reports upon an empirical study aiming at investigating the influence of employing the Z specification notation upon how users approach system development. The study illustrates how the desire to employ formality can have a significant influence upon preferred choice between different solution approaches. Despite the formal representation increasing the awareness of the characteristics of a given design problem, the notation is apparently detrimental in the subjects' consideration of good-quality generic solutions. The human factor issues of the notation need to be carefully considered and the notation should be embedded into a proper method if effective use is to be achieved.     

Reliable parallel software construction using PARSE

The PARSE design methodology provides a hierarchical, object-based approach to the development of parallel software systems. A system design is initally structured into a collection of concurrently executing objects which communicate via message-passing. A graphical notation known as the process graph is then used to capture the structural and important dynamic properties of the system. Process graph designs can then be semi-mechanically transformed into complete Petri nets to give a detailed, executable and potentially verifiable design specification. From a complete design, translation rules for target programming languages are defined to enable the implementation to proceed in a systematic manner. The paper describes the steps in PARSE methodology and process graph notation, and illustrates the application of PARSE from design specification to program code using a network protocol example.     

Foundations of the trace assertion method of module interfacespecification

The trace assertion method is a formal state machine based method for specifying module interfaces. A module interface specification treats the module as a black-box, identifying all the module's access programs (i.e., programs that can be invoked from outside of the module) and describing their externally visible effects. In the method, both the module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of nondeterminism, normal and exceptional behavior, value functions, and multiobject modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted     

A framework for specification-based testing

Test templates and a test template framework are introduced as useful concepts in specification-based testing. The framework can be defined using any model-based specification notation and used to derive tests from model-based specifications-in this paper, it is demonstrated using the Z notation. The framework formally defines test data sets and their relation to the operations in a specification and to other test data sets, providing structure to the testing process. Flexibility is preserved, so that many testing strategies can be used. Important application areas of the framework are discussed, including refinement of test data, regression testing, and test oracles     

Mathematical notation in formal specification: too difficult forthe masses?

The phrase “not much mathematics required” can imply a variety of skill levels. When this phrase is applied to computer scientists, software engineers, and clients in the area of formal specification, the word “much” can be widely misinterpreted with disastrous consequences. A small experiment in reading specifications revealed that students already trained in discrete mathematics and the specification notation performed very poorly; much worse than could reasonably be expected if formal methods proponents are to be believed     

Providing Architectural Languages and Tools Interoperability through Model Transformation Technologies

Many architectural languages have been proposed in the last 15 years, each one with the chief aim of becoming the ideal language for specifying software architectures. What is evident nowadays, instead, is that architectural languages are defined by stakeholder concerns. Capturing all such concerns within a single, narrowly focused notation is impossible. At the same time, it is also impractical to define and use a “universal” notation, such as UML. As a result, many domain-specific notations for architectural modeling have been proposed, each one focusing on a specific application domain, analysis type, or modeling environment. As a drawback, a proliferation of languages exists, each one with its own specific notation, tools, and domain specificity. No effective interoperability is possible to date. Therefore, if a software architect has to model a concern not supported by his own language/tool, he has to manually transform (and, eventually, keep aligned) the available architectural specification into the required language/tool. This paper presents DUALLy, an automated framework that allows architectural languages and tools interoperability. Given a number of architectural languages and tools, they can all interoperate thanks to automated model transformation techniques. DUALLy is implemented as an Eclipse plugin. Putting it in practice, we apply the DUALLy approach to the Darwin/FSP ADL and to a UML2.0 profile for software architectures. By making use of an industrial complex system, we transform a UML software architecture specification in Darwin/FSP, make some verifications by using LTSA, and reflect changes required by the verifications back to the UML specification.     

A scenario-matching approach to the description and model checking of real-time properties

A major obstacle in the technology transfer agenda of behavioral analysis and design methods is the need for logics or automata to express properties for control-intensive systems. Interaction-modeling notations may offer a replacement or a complement, with a practitioner-appealing and lightweight flavor, due partly to the sub specification of intended behavior by means of scenarios. We propose a novel approach consisting of engineering a new formal notation of this sort based on a simple compact declarative semantics: VTS (visual timed event scenarios). Scenarios represent event patterns, graphically depicting conditions over traces. They predicate general system events and provide features to describe complex properties not expressible with MSC-like notations. The underlying formalism supports partial orders and real-time constraints. The problem of checking whether a timed-automaton model has a matching trace is proven decidable. On top of this kernel, we introduce a notation to state properties over all system traces: conditional scenarios, allowing engineers to describe uniquely rich connections between antecedent and consequent portions of the scenario. An undecidability result is presented for the general case of the model-checking problem over dense-time domains, to later identify a decidable-yet practically relevant-subclass, where verification is solvable by generating antiscenarios expressed in the VTS-kernel notation.