Vibes: A visual language for specifying behavioral requirements of algorithms

Manually verifying the behavior of software systems with respect to a set of requirements is a time-consuming and error-prone task. If the verification is automatically performed by a model checker however, time can be saved, and errors can be prevented. To be able to use a model checker, requirements need to be specified using a formal language. Although temporal logic languages are frequently used for this purpose, they are neither commonly considered to have sufficient usability, nor always naturally suited for specifying behavioral requirements of algorithms. Such requirements can be naturally specified as regular language recognizers such as deterministic finite accepters, which however suffer from poor evolvability: the necessity to re-compute the recognizer whenever the alphabet of the underlying model changes. In this paper, we present the visual language Vibes that both is naturally suited for specifying behavioral requirements of algorithms, and enables the creation of highly evolvable specifications. Based on our observations from controlled experiments with 23 professional software engineers and 21 M.Sc. computer science students, we evaluate the usability of Vibes in terms of its understandability, learnability, and operability. This evaluation suggests that Vibes is an easy-to-use language.     

E<Emphasis Type="SmallCaps">ssence</Emphasis>: A constraint language for specifying combinatorial problems

Essence is a formal language for specifying combinatorial problems in a manner similar to natural rigorous specifications that use a mixture of natural language and discrete mathematics. Essence provides a high level of abstraction, much of which is the consequence of the provision of decision variables whose values can be combinatorial objects, such as tuples, sets, multisets, relations, partitions and functions. Essence also allows these combinatorial objects to be nested to arbitrary depth, providing for example sets of partitions, sets of sets of partitions, and so forth. Therefore, a problem that requires finding a complex combinatorial object can be specified directly by using a decision variable whose type is precisely that combinatorial object.     

Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language

We present an algorithm for the translation of security protocol specifications in the HLPSL language developed in the framework of the AVISPA project to a dialect of the applied pi calculus. This algorithm provides us with two interesting scientific contributions: at first, it provides an independent semantics of the HLPSL specification language and, second, makes it possible to verify protocols specified in HLPSL with the applied pi calculus-based ProVerif tool. Our technique has been implemented and tested on various security protocols. The translation can handle a large part of the protocols modelled in HLPSL.     

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 SystemC library for specifying pipeline abstractions

We describe a SystemC library for specifying, modeling, and simulating hardware pipelines. The library includes a set of overloaded operators defining a pipeline expression language that allows the user to quickly specify the architecture of the pipeline. The pipeline expression is used to derive the connectivity of the SystemC modules that define the stages of the pipeline and to automatically insert latches and control modules between the stages to handle the proper routing of transactions through pipeline. Using the SystemC simulator the pipeline can then be simulated and evaluated. The pipeline expression language sits on top of SystemC, exposes all of the features of C++ and SystemC enabling the user to specify, evaluate, and analyze pipeline architectures.     

A language for specifying program transformations

A language is described for specifying program transformations, from which programs can be generated to perform the transformations on sequences of code. The main objective of this work has been to develop a language that would allow the user to quickly and easily specify a wide range of transformations for a variety of programming languages. The rationale for the language constructs is given, as well as the details of an implementation which was prototyped using Prolog. Numerous examples of the language usage are provided     

The living in a lattice rule language

This paper presents a rule-based query language for an object-oriented database model. The database model supports complex objects, object identity, classes and types, and a class/type hierarchy. The instances are described by ‘object relations’ which are functions from a set of objects to value sets and other object sets. The rule language is based on object-terms which provide access to objects via the class hierarchy. Rules are divided into two classes: object-preserving rules manipulating existing objects (yielding a new ‘view’ on objects available in the object base) and object-generating rules creating new objects with properties derived from existing objects. The derived object sets are included in a class lattice. We give conditions for whether the instances of the ‘rules’ heads are ‘consistent’, i.e. represent object relations where the properties of the derived objects are functionally determined by the objects.     

EQL: A language for numerical computation

EQL, a language for numerical computation, has been implemented. This paper describes essential properties of the EQL language, which considerably simplifies numerical analysis and programming thanks to the following features: (1) elimination of explicit sequencing: (2) matrix and array computations: (3) simple and convenient notation of iteration procedure: (4) mapping of data structures (vector or matrix) on data objects which are represented in the computer: (5) tabulation facility for function values. Also the outline of translator, which transforms an EQL program to FORTRAN codes, is described.     

Graphical scenarios for specifying temporal properties: an automated approach

Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these formalisms too often represents an impediment to move these techniques from “research theory” to “industry practice”. The objective of this work is to facilitate the nontrivial and error prone task of specifying, correctly and without expertise in temporal logic, temporal properties. In order to understand the basis of a simple but expressive formalism for specifying temporal properties we critically analyze commonly used in practice visual notations. Then we present a scenario-based visual language called Property Sequence Chart (PSC) that, in our opinion, fixes the highlighted lacks of these notations by extending a subset of UML 2.0 Interaction Sequence Diagrams. We also provide PSC with both denotational and operational semantics. The operational semantics is obtained via translation into Büchi automata and the translation algorithm is implemented as a plugin of our Charmy tool. Expressiveness of PSC has been validated with respect to well known property specification patterns. Preliminary results appeared in (Autili et al. 2006a).     

Dispel: A run-time debugging language

Dispel is a language designed to aid communication between an interactive user and a run-time, symbolic debugging system. Important attributes of Dispel are that it provides a small set of primitive debugging actions, most traditional debugging aids (such as variable traces and postmortem dumps) are written in terms of these primitives as debugging routines, and Dispel serves both as an interactive debugging command language and as a special-purpose programming language. The syntax and semantics of Dispel are explained and examples of Dispel commands and routines are presented.     

A formal notation for specifying static semantic rules

The syntax rules of programming language are generally fairly well understood and may easily be expressed formally as a grammar using BNF. However, the static semantic rules are less well understood and considerably more difficult to express formally. All notations for expressing static semantic rules either formally or informally involve actions being associated with the productions of the grammar. This paper presents such a formal notation which has been applied to various languages and found to be very useful both for the designer and the compiler writer.     

LASS: A language for stochastic systems

A new problem oriented language for finding solutions to problems to probability theory is presented. A system is first described as a structure of probabilistic cause and effect relationships. The, questions concerning outcome probabilities are posed. The programming system then provides exact answers to such questions by applying discrete probability theory.     

Methods for specifying static semantics

The formal specification of a programming language involves the specification of three types of rules: syntax, static semantics and semantics. Various methods have been proposed for specifying the static semantic rules of programming languages, but as yet no method has received general acceptance. This paper looks at several different specification techniques and attempts to isolate the basic mechanisms used by each of them and explain the pattern of development of specification techniques for static semantics.     

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.     

Very high-level language design: A viewpoint

Recent developments in very high-level language design indicate that these languages hold great promise for improving the level of man-machine communication, and hence improving computer and programmer utilization. (Essentially, a very high-level language one which allows the programmer to specify what to do, rather than how to do it.) This paper surveys these developments, outlines the goals to which an “ideal” very high-level language should aspire, and then presents the design of a very high-level language that would meet these goals. This design is presented in the interest of laying bare some basic design and implementation questions that are inherent to such an achievement. The paper then discusses these questions, indicating both old and new research problems which they suggest.     

Neverlang: A framework for feature-oriented language development

Reuse in programming language development is an open research problem. Many authors have proposed frameworks for modular language development. These frameworks focus on maximizing code reuse, providing primitives for componentizing language implementations. There is also an open debate on combining feature-orientation with modular language development. Feature-oriented programming is a vision of computer programming in which features can be implemented separately, and then combined to build a variety of software products. However, even though feature-orientation and modular programming are strongly connected, modular language development frameworks are not usually meant primarily for feature-oriented language definition. In this paper we present a model of language development that puts feature implementation at the center, and describe its implementation in the Neverlang framework. The model has been evaluated through several languages implementations: in this paper, a state machine language is used as a means of comparison with other frameworks, and a JavaScript interpreter implementation is used to further illustrate the benefits that our model provides.     

PIT: A macro-implemented implementation language

An implementation technique called PIT, for pseudo instructional technique, is described which utilizes the macro capabilities of most macro assemblers. A low level machine architecture is described via a set of macros that include some ‘high level’ features. Since the macros manipulate computer words, and refer to actual registers, their implementation in a system is relatively efficient, but since they do not reflect any one particular hardware design, they can be implemented by almost any macro assembler. Tests are built into the macros so that a PIT program will run without change on any machine that has defined these macros This technique should provide an alternative to using higher level languages as implementation languages if the object code produced by those compilers is deemed too slow (or too large) for the application that is being programmed.     

Fibonacci: A programming language for object databases

Fibonacci is an object-oriented database programming language characterized by static and strong typing, and by new mechanisms for modeling data-bases in terms of objects with roles, classes, and associations. A brief introduction to the language is provided to present those features, which are particularly suited to modeling complex databases. Examples of the use of Fibonacci are given with reference to the prototype implementation of the language.