Modechart: a specification language for real-time systems

Present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of real-time logic (RTL), which is especially amenable to reasoning about the absolute (real-time clock) timing of events. The semantics of Modechart has an important property that the translation of a Modechart specification into RTL formulas results in a hierarchical organization of the resulting RTL assertions. This gives us significant leverage in reasoning about properties of a system by allowing us to filter out assertions that concern lower levels of abstraction. Some results about desirable properties of Modechart specifications are given. A graphical implementation of Modechart has been completed     

An interpreter for LOTOS,a specification language for distributed systems

LOTOS is an executable specification language for distributed systems currently being standardized within ISO as a tool for the formal specification of open systems interconnection protocols and services. It is based on an extended version of Milner's calculus of communicating systems (CCS) and on ACT ONE abstract data type (ADT) formalism. A brief introduction to LOTOS is given, along with a discussion of LOTOS operational semantics, and of the executability of LOTOS specifications. Further, an account of a prototype LOTOS interpreter is given, which includes an interactive system that allows the user to direct the execution of a specification (for example, for testing purposes). The interpreter was implemented in YACC/LEX, C and Prolog. The following topics are discussed: syntax and static semantics analysis; translation from LOTOS external format to internal representation; evaluation of ADT value expressions and extended CCS behaviour expressions. It is shown that the interpreter can be used in a variety of ways: to recognize whether a given sequence of interactions is allowed by the specification; to generate randomly chosen sequences of interactions; in a user-guided generation mode, etc.     

A familial specification language for database application systems

The Familial Specification Language is a set theoretic and functional language providing a unified approach to the less-procedural design of database application systems. The language is proposed to be both a database language and an application program specification language. The unique data structure employed, the family of sets, provides the designer with a unified framework, both to model and maintain data, and to algebraically specify the application programs without looping or branching, and with no side effects. Using the same data structure in both the data model and the problem specification creates a natural interface between the database and the application programs. Special emphasis is placed on aggregation and classification, the major problems is business data processing.     

Formal methods for analysis of discrete systems using a specification language

A realization of an algorithm that translates an MSC diagram (an MSC document) into an event equivalent Petri net is described, and the correctness of the algorithm is proved. The net obtained in this way can be used to analyze properties of the original MSC document. The mentioned algorithm is a part of a system designed for verification and analysis of MSC documents. Translated from Kibernetika i Sistemnyi Analiz, No. 4, pp. 31–56, July–August 2009.     

GSL: a requirements specification language for end-user intelligibility

Software Requirements Specifications (SRS) have been used to fill the communication gap between systems analysts and the end-users. SRSs should satisfy the needs of both systems analysts and end-users. Non-technical end-users require intelligible SRSs while systems analysts need more precise, clear and concise SRSs. Object-oriented methods cannot represent temporal relations between events precisely. However, object-oriented principles are widely used in systems analysis and designing. Hence, there is a need for a software requirements specification language which supports object-oriented analysis methods, represents temporal knowledge precisely and whose representation scheme resembles natural languages. The specification language presented in this paper, GSL, is designed to meet the above requirements. The language is based on First-order Temporal Logic (FTL), which has temporal operators in addition to classical logical connectives and quantifiers. Since FTL cannot represent relative temporal knowledge and it inherits problems with point-based time models, a new logical connective TAND and redefined AND connective are used to represent relative temporal knowledge and to solve the problems with FTL. The language employs object-oriented principles: events, conditions, rules and activities can be represented as objects as well as attributes of an object. However, systems analysts can decide whether to use object-oriented conceptual modeling or not. © 1998 John Wiley & Sons, Ltd.     

SWSL: a synthetic workload specification language for real-timesystems

We discuss the issues that must be addressed in the specification and generation of synthetic workloads for distributed real-time systems. We describe a synthetic workload specification language (SWSL) that defines a workload in a form that can be compiled by a synthetic workload generator (SWG) to produce an executable synthetic workload. The synthetic workload is then downloaded to the target machine and executed while performance and dependability measurements are made. SWSL defines the workload at the task level using a data flow graph, and at the operation level using control constructs and synthetic operations taken from a library. It is intended to be easy to use, flexible, and capable of creating synthetic workloads that are representative of real-time workloads. It provides a compact, parameterized notation. It supports automatic replication of objects to facilitate the specification of large workloads for distributed real-time systems. It also provides extensive support for the experimentation process     

A requirement specification language for configuration dynamics of multiagent systems

In agent‐mediated applications, the system configuration can change because of the creation and the deletion of agents. The behavior of such systems on the one hand depends on the dynamics of the system configuration; on the other hand, behavior of such a system consists of the information dynamics of the system. We discuss configuration and information dynamics of agent‐mediated systems and define a requirement language to express properties of those dynamics. A prototypical scenario for an agent‐mediated system is discussed and some important requirements for this system are specified. It is shown how these properties can be verified automatically to evaluate system behavior. © 2004 Wiley Periodicals, Inc.     

A parallel logic language for transaction specification in multidatabase systems

The realization of truly heterogeneous database systems is hampered by two principal obstacles. One is the unsuitability of traditional transaction models; this has led to the proposal of a number of new, advanced transaction models. The second is the lack of appropriate programming support for these advanced concepts. This paper addresses these two issues by pointing out the advantages of using a logic-based approach for the integration of autonomous software systems.The work is supported by the Austrian FWF (Fonds zur Förderung der wissenschaftlichen Forschung), project Multidatabase Transaction Processing, contract number P09020-MAT.     

DEVSpecL: DEVS specification language for modeling,simulation and analysis of discrete event systems

Discrete EVent Systems Specification (DEVS) formalism supports specification of discrete event models in a hierarchical modular manner. This paper proposes a DEVS modeling language called DEVS Specification Language (DEVSpecL) based on which discrete event systems are modeled, simulated and analyzed within a DEVS-based framework for seamless systems design. Models specified in DEVSpecL can be translated in different forms of codes by code generators, which are executed with various tools for models verification, logical analysis, performance evaluation, and others.     

BDL: a specialized language for per-object reactive control

The problem of describing the concurrent behavior of objects in object oriented languages is addressed. The approach taken is to let methods be the behavior units whose synchronization is controlled separate from their specification. Our proposal is a domain-specific language called BDL for expressing constraints on this control and actually implementing its enforcement. We propose a model where each object includes a so-called “execution controller”, programmed in BDL. This separates cleanly the concepts of what the methods do, the object processes, from the circumstances in which they are allowed to do it, the control. The object controller ensures that scheduling constraints between the object's methods are met. Aggregate objects can be controlled in terms of their components. This language has a convenient formal base. Thus, using BDL expressions, behavioral properties of objects or groups of interesting objects can be verified. Our approach allows, for example, deadlock detection or verification of safety properties, while maintaining a reasonable code size for the running controller. A compiler from BDL has been implemented, automatically generating controller code in an Esterel program, i.e., in a reactive programming language. From this code, the Esterel compiler, in turn, generates an automaton on which verifications are done. Then this automaton is translated into a C code to be executed. This multistage process typifies the method for successful use of a domain-specific language. This also allows high level concurrent programming     

Design Rationale for a Wide Spectrum Specification Language FGSPEC

FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification whic describes “what to do ”to the corresponding design(perational)specification whic describer“how to do ”.The design emphasizes the coherence of multi-level specification mechanisms and a tree structure model is provided whic unifies the wide spectrum specification styles from“what”to“how”.     

A verification framework for spatio-temporal consistency language with CCSL as a specification language

The Spatio-Temporal Consistency Language(STeC)is a high-level modeling language that deals natively with spatio-temporal behaviour,i.e.,behaviour relating to certain locations and time.Such restriction by both locations and time is of first importance for some types of real-time systems.CCSL is a formal specification language based on logical clocks.It is used to describe some crucial safety properties for real-time systems,due to its powerful expressiveness of logical and chronometric time constraints.We consider a novel verification framework combining STeC and CCSL,with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints.We propose a theory combining these two languages and a method verifying CCSL properties in STeC models.We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.     

Functional specification and proof of correctness for time dependent behaviour of reactive systems

A functional formalism for describing and reasoning about the time dependent behaviour of reactive systems is presented. The model is event based and can describe the histories of events with finite duration. It is a generalisation of the model of Caspi and Halbwachs (1986). A set of tools with their operations are introduced in the formalism and structure theorems characterising the algebra of events are proved. The power of this extended model is illustrated through the formal specification and correctness proof for a problem chosen from robotics.     

H: A component-based specification language for heterogeneous applications

This paper presents H, a minimalistic specification language for designing heterogeneous software applications, particularly in the realms of robotics and industria, which takes advantage of a Component-Based Software Engineering (CBSE) approach. H copes with some of the most outstanding characteristics of these systems, like diversity at different levels (hardware platforms, programming languages, programmer skills), network distribution, real time and fault-tolerance. The H specification covers the life-cycle of any heterogeneous application. Its development system offers to the designer and/or builder a set of tools for specifying modules, generating code semiautomatically, debugging, maintenance, and a real time analysis of the system.     

The development of a specification language for a computer security system

The primary goal of this paper is to define an initial step towards the definition of ‘systems grammar’ based on the notion of formal languages which can be used as a ‘tool’ in the formal representation of computer security systems. Currently all modelling done on computer security systems is written up as mathematical models. These mathematical models are usually based on the mathematics of relations amongst objects, as opposed to the model described in this paper which is based on the theory of formal languages. This paper is aimed at people who are doing research on the logical aspects of computer security. It is the first of a series of two papers. This paper will give interim results and make more specific the definition of a ‘formal language’ which suits the computer security environment. The second paper will illustrate the actual use of the defined ‘formal language’ and show how to represent the characteristics of a computer security environment by using this ‘formal language’.     

Behavioral specification of reactive systems using stream-based I/O tables

A core problem in formal methods is the transition from informal requirements to formal specifications. Especially when specifying the behavior of reactive systems, many formalisms require the user to either understand a complex mathematical theory and notation or to derive details not given in the requirements, such as the state space of the problem. For many approaches also a consistent set of requirements is needed, which enforces to resolve requirements conflicts prior to formalization. This paper describes a specification technique, where not states but signal patterns are the main elements. The notation is based on tables of regular expressions and supports a piece-wise formalization of potentially inconsistent requirements. Many properties, such as input completeness and consistency, can be checked automatically for these specifications. The detection and resolution of conflicts can be performed within our framework after formalization. Besides the formal foundation of our approach, this paper presents prototypical tool support and results from an industrial case study.     

Interpretable program specification language

In the paper, a domain-specific language of executable specifications is proposed. This language makes it possible to describe models of formalized subject domains in a graphical form, formulate computational problems on these models, and synthesize programs for solving these problems (including parallel ones) based on deductive inference in a special class of proposition calculus.     

SoC系统级描述语言SpecC

讨论了SoC系统描述的要求,针对这些要求指出了目前系统级描述语言的不足之处,然后分别从层次化,同步、异常处理、时序等几个方面详细介绍一种能满足SoC系统所有描述要求的系统级描述语言--SpecC语言.将SpccC语言和其它系统级描述语言在系统描述能力和可综合性等多个方面进行比较,结果表明,SpecC语言在系统级描述方面具有明显的优势.