Giving semantics to SA/RT by means of high-level timed Petri nets

In the IPTES project a dual language approach is proposed for overcoming both the problems derived from the use of a user-friendly, high-level, but not-formally-defined language and from a lower-level, formal, but difficult-to-use language. The approach uses a user-friendly, high-level language as user interface and a lower-level, formal language asmachine language. In this way the users can both access the IPTES environment through a nice interface and can profit from non-ambiguity-checks and proofs algorithms based on the formal kernel machine language. The correspondence between the two languages is built-in in the IPTES environment that provides a transparent mapping mechanism that relates the users specifications expressed by means of the high-level interface-language with the formal definitions expressed in the formal machine language.This paper presents the mapping mechanism that relates the current IPTES user interface (SA/RT (Ward and Mellor 1985)) with the IPTES machine language (high-level timed Petri nets (Ghezzi, Mandrioli, Morasca and Pezzé 1991)). As a side effect, it also presents the formal semantics of SA/RT defined by means of high-level timed Petri nets.This material is based upon work supported by the CEC under the ESPRIT program project no. EP5570 IPTES, by the Piano Finalizzato Sistemi Informatici e Calcolo Parallelo (CNR) and by The Technical Development Centre of Finland (TEKES).     

PLCTOOLS: Graph Transformation Meets PLC Design

This paper presents PLCTOOLS, a formal environment for designing and simulating programmable controllers. Control models are specified with IEC FED (Function Block Diagram), and translated into functionally equivalent HLTPNs (High-Level Timed Petri Nets), through MetaEnv, for analysis and simulation and obtained results are presented in terms of suitable animations of FED blocks.The peculiarity with FBD is that it does not come with a fixed set of syntactic elements; it allows users to add as many new blocks as they want. Consequently, each time users want to add a new FBD block with PLCTOOLS, they must provide the concrete syntax, to add it to the library of available blocks, but also the associated HLTPN, to allow MetaEnv to build the formal representation.     

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.     

An executable subset of VDM-SL in an SA/RT framework

In this article we present the executable specification language IPTES Meta-IV based on the formal specification language VDM-SL. The language has been fitted to work in an SA/RT framework and the article presents how it supports the specification of the data transformation part of SA/RT. Furthermore we present some of the advanced constructs of the language seen as an executable specification language in its own right. Finally we present how an IPTES Meta-IV interpreter is used in combination with a high-level timed Petri net executor to execute SA/RT models.     

Semantics,calculi, and analysis for object-oriented specifications

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.     

Specification of realtime systems using ASTRAL

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the rationale of ASTRAL's design. ASTRAL's specification style is illustrated by discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a composition section, which provides the needed information to combine two or more ASTRAL system specifications     

Coincidental extension of scattered context languages

For a symbol, #, and a string, x = a ₁ a ₂ ...a _{n - 1} a _n , any string of the form # ⁱ a ₁ # ⁱ a ₂ # ⁱ...# ⁱ a _{n - 1} # ⁱ a _n # ⁱ, where 0, is a coincidental #-extension of x. A language, K, is a coincidental #-extension of L if every string of K represents a coincidental extension of a string in L and the deletion of all #s in K results in L. This paper proves that for every recursively enumerable language, E, there exists a propagating scattered context language that represents a coincidental extension of E. Received: 31 October 2001 / 31 January 2003     

IPTES: A concurrent engineering approach for real-time software development

The constantly increasing concurrency, complexity, and risks associated with the industrial development of real-time embedded computer systems has been approached in different ways in recent years. In Esprit project no. EP5570, called IPTES, a methodology and a supporting environment to support the Boehm's spiral process are being developed. The prototyping environment will enable the specification, development, and verification of executable system models so that different parts of the system may represent different modeling levels and yet can be executed as a total system. Concurrent engineering problems in connection with multi-supplier, distributed software development are also addressed in the IPTES environment. In the IPTES project the concept of heterogeneous prototyping is proposed as a solution. Each of the development teams may use relatively abstract models of the other parts of the systems as a testbed (environment model) for their own part, yet they can proceed developing their own part full speed by means of advancing the maturity of their part to the next abstraction level(s). The IPTES environment provides a set of tools to help in the process of creating, analyzing, and testing distributed heterogeneous prototypes.     

Towards the formal specification of an OPS5 production system architecture

The article presents a formal specification for many important aspects of the OPS5 production systems framework. the article illustrates how an abstract formal specification of a production system can be created and the benefits this provides to those involved in the development of knowledge-based systems. the formal specification is preceded by an informal specification of a production system upon which the formal model is based and the development is illustrated through the use of concrete examples. the notation used is that of “Z” (J. M. Spivey, The Z Notation, Prentice-Hall, Englewood Cliffs, NJ, 1990), a language based upon typed set theory. This language has been used to success in the specification of critical conventional software systems (I. Hayes, Technical Monograph PRG-46, Oxford University Computing Laboratory, Oxford, England, 1985) and which is formal enough to allow for the creation of rigorous specifications, yet is of a form that makes these specifications “readable.” the aim of the article is to show that formal techniques can be applied to areas of knowledge-based system development, thus promoting correctness, reliability, and understanding. © 1994 John Wiley & Sons, Inc.     

Compositional semantics of a real-time prototyping language

The formal semantics of a prototyping language for hard real-time systems, PSDL, is given. PSDL provides a data flow notation augmented by application-orientation timing and control constraints to describe a system as a hierarchy of networks of processing units communicating via data streams. The semantics of PSDL are defined in terms of algebraic high-level Petri nets. This formalism combines algebraic specifications of abstract data types with process and concurrency concepts of Petri nets. Its data abstraction facilities are used to define the meaning of PSDL data types, while high-level Petri nets serve to model the casual and timing behavior of a system. The net model exposes potential concurrency of computation and makes all synchronization needs implied by timing and control constraints explicit and precise. Time is treated as state of clocks, and clocks are modeled as ordinary system components. The net semantics provides the basis for applying analysis techniques and semantic tools available for high-level Petri nets     

The design and analysis of real-time systems using the ASTRAL software development environment

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the ASTRAL Software Development Environment (SDE), which is an integrated set of design and analysis tools based on the ASTRAL formal framework. The tools that make up the support environment are a syntax-directed editor, a specification processor, a verification condition generator, a browser kit, a model checker, and a mechanical theorem prover. This revised version was published online in June 2006 with corrections to the Cover Date.     

A formal and sound transformation from Focal to UML: an application to airport security regulations

We propose an automatic transformation of Focal specifications to UML class diagrams. The main motivation for this work lies within the framework of the EDEMOI project, which aims to integrate and apply several requirements engineering and formal methods techniques to analyze airport security regulations. The idea is to provide a graphical documentation of formal models for developers, and in the long-term, for certification authorities. The transformation is formally described and an implementation has been designed. We also show how the soundness of our approach can be achieved.     

Towards meaning-based machine translation: using abstractions from text generation for preserving meaning

One of the primary motivations of text generation is the achievement of a very wide range of linguistic abilities coupled with functional control of that range. This control rests on the appropriate construction of abstract specifications of meaning that can guide the generation process to produce language that is textually, grammatically, and lexically appropriate. Such abstract semantic specifications, when constructed in the right way, preserve much of the meaning required in a translation without unduly constraining syntactic form. This is potentially of great value for machine translation since it opens up the possibility of domain-independent, constrained, meaning-based translation. This paper describes how the upper model of the PENMAN text generation system provides a level of semantic abstraction of this kind. It offers examples of the motivation of broader sets of likely translational equivalents than that possible with transfers at lower-levels of abstraction and sets out types of constraints by which the set of likely translational equivalents may be reduced to high-quality renderings of the source text.     

Executable formal specifications of complex distributed systems with CoreASM

Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be. With increasing complexity of software-intensive computer-based systems and the challenges of validation and verification of abstract software models prior to coding, the need for interactive software tools supporting executable formal specifications is even more evident. In this paper, we discuss how CoreASM, an environment for writing and running executable specifications according to the ASM method, provides flexibility and manages the complexity by using an innovative extensible language architecture.     

Formal Modeling and Reconfiguration of User Interfaces for Reduction of Errors in Failure Handling of Complex Systems

Controlling and observing complex systems is central to the study of human–machine interaction. In our understanding, there is much to be gained from integrating formal modeling and analysis, including the reconfiguration of user interfaces, with the development of user interfaces with high usability. To this end, we introduce a new approach to modeling and reconfiguration of user interfaces jointly with a newly developed set of tools for interactive and visual creation and automatic transformation of user interfaces' interaction logic to a formal language based on Petri nets. Reconfiguration will be embedded into a process for adapting user interfaces to the user's cognitive representation of the controlled system. This process involves practicing the use of a given user interface, adapting it to the user's needs through reconfiguration, and applying the resulting adaptations to the formally defined interaction logic. An evaluation study confirms that this process reduces errors in interaction.