From algebraic semantics to denotational semantics for Verilog

This paper considers how the algebraic semantics for Verilog relates with its denotational semantics. Our approach is to derive the denotational semantics from the algebraic semantics. We first present the algebraic laws for Verilog. Every program can be expressed as a guarded choice that can model the execution of a program. In order to investigate the parallel expansion laws, a sequence is introduced, indicating which instantaneous action is due to which exact parallel component. A head normal form is defined for each program by using a locality sequence. We provide a strategy for deriving the denotational semantics based on head normal form. Using this strategy, the denotational semantics for every program can be calculated. Program equivalence can also be explored by using the derived denotational semantics. A short version of this paper appeared in Proc. ICECCS 2006: 11th IEEE International Conference on Engineering of Complex Computer Systems [48]. This work is partially supported by the National Basic Research Program of China (No. 2005CB321904), the National High Technology Research and Development Program of China (No. 2007AA010302) and the National Natural Science Foundation of China (No. 90718004). Jonathan Bowen is a visiting professor at King’s College London and an emeritus professor at London South Bank University.     

An algebraic semantics of higher-order types with subtypes

This paper extends order-sorted algebras with higher-order functions. The aim is to present a new semantics for higher-order order-sorted types in functional programming, data type specification and program transformation. Our framework unifies higher-order functions, equational deduction, overloading and subtype polymorphism.     

Program transformations and algebraic semantics

We study transformations and equivalences of recursive program schemes. We give an optimization algorithm which recognizes and removes all parts of a program scheme which do not affect its final output. This result leads to a syntactic way of suppressing some erroneous loops in programs and can be used to prove that equivalence of recursive program schemes is solvable under particular conditions.     

Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Complex software systems typically involve features like time, concurrency and probability, with probabilistic computations playing an increasing role. However, it is currently challenging to formalize languages incorporating all those features. Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. (2006, 2009) [51] and [53]), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC, highlighting both its theoretical and practical aspects.The link is obtained by deriving the operational semantics from the algebraic semantics, an approach that may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws are provided that suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from the algebraic semantics, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operational semantics with respect to the algebraic semantics.That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, the generation of head normal form is explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy that exploits head normal form. The operational semantics is also animated. These animations, which again supports to claim soundness and completeness of the operational semantics with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results.     

A Continuous Algebraic Semantics of CSP

This is an attempt to use continuous algebras to describe the semantics of CSP-continuity being used to solve recursive definitions of processes as infinite objects.By so doing,we combine the algebraic specifications of abstract data types with CSP 50 make ups 2 new language,which is recommended as a promising candidate of specification language for designing and developing communicating systems.     

An operational semantics for Stateflow

We present a formal operational semantics for Stateflow, the graphical Statecharts-like language of the Matlab/Simulink tool suite that is widely used in model-based development of embedded systems. Stateflow has many tricky features but our operational treatment yields a surprisingly simple semantics for the subset that is generally recommended for industrial applications. We have validated our semantics by developing an interpreter that allows us to compare its behavior against the Matlab simulator. We have used the semantics as a foundation for developing prototype tools for formal analysis of Stateflow designs.     

Inductive inference of logic programs based on algebraic semantics

In this paper we present a new inductive inference algorithm for a class of logic programs, calledlinear monadic logic programs. It has several unique features not found in Shapiro’s Model Inference System. It has been proved that a set of trees isrational if and only if it is computed by a linear monadic logic program, and that the rational set of trees is recognized by a tree automaton. Based on these facts, we can reduce the problem of inductive inference of linear monadic logic programs to the problem of inductive inference of tree automata. Further several efficient inference algorithms for finite automata have been developed. We extend them to an inference algorithm for tree automata and use it to get an efficient inductive inference algorithm for linear monadic logic programs. The correctness, time complexity and several comparisons of our algorithm with Model Inference System are shown.     

An executable formal semantics for UML-RT

We propose a formal semantics for UML-RT, a UML profile for real-time and embedded systems. The formal semantics is given by mapping UML-RT models into a language called kiltera, a real-time extension of the \(\pi \)-calculus. Previous attempts to formalize the semantics of UML-RT have fallen short by considering only a very small subset of the language and providing fundamentally incomplete semantics based on incorrect assumptions, such as a one-to-one correspondence between “capsules” and threads. Our semantics is novel in several ways: (1) it deals with both state machine diagrams and capsule diagrams; (2) it deals with aspects of UML-RT that have not been formalized before, such as thread allocation, service provision points, and service access points; (3) it supports an action language; and (4) the translation has been implemented in the form of a transformation from UML-RT models created with IBM’s RSA-RTE tool, into kiltera code. To our knowledge, this is the most comprehensive formal semantics for UML-RT to date.     

An algebraic technique for context-sensitive parsing

A technique that represents derivations of a context-free grammarG over a semiring and that obtains for a wordw inL(G) the set of all canonical parses forw has previously been described. A state grammar is one of a collection of grammars that place restrictions on the manner of application of context-free-like productions and that generate a noncontext-free language. The context-free properties of a state grammar have been used to extend the algebraic parsing technique for languages generated by state grammars,viz., context-sensitive languages. The extension for state grammars is not unlike that required for other types of grammars in whose collection state grammars are representative.     

An algebraic model for programming languages

The language of universal algebras is used as a model for programming language specification. BNF rules are employed for specifying the signature of the language algebra instead of the context free syntax. The algorithm for program evaluation is inductively defined by the following universal algebraic construction:

Any function defined on the generators of a free algebra taking values in the carrier of another similar algebra can be uniquely extended to a homomorphism between the two algebras.

Any conventional programming language can be specified by a finite set of BNF rules and its algebra of symbols is generated by a finite set of generator classes. Thus any function defined on the finite set of generators offers an algebraic mechanism for a universal algorithm for source language program evaluation.     

DATAPLAN: An interface generator for database semantics

A model system ( called DATAPLAN) is proposed for generation, access, and control of a shared database by casual users in their own terminology. The DATAPLAN system achieves this goal by planning a dialog which hierarchically defines the possible universe of discourse where casual users can communicate with the database. The plan is executed on the domains of hierarchical semantics, and controlled by pattern matching with a goal and generative backtracking mechanism. To ensure flexible and smooth communication of casual users with the shared database, the system generates individualized user class “fuzzy” interfaces. They are composed of multiplex associations of the attributes and values of the shared database with those of casual user classes in varying degrees.     

An operational semantics for a calculus for wireless systems

In wireless systems, the communication mechanism combines features of broadcast, synchrony, and asynchrony. We develop an operational semantics for a calculus of wireless systems. We present different Reduction Semantics and a Labelled Transition Semantics and prove correspondence results between them. Finally, we apply CWS to the modelling of the Alternating Bit Protocol, and prove a simple correctness result as an example of the kind of properties that can be formalized in this framework.A major goal of the semantics is to describe the forms of interference among the activities of processes that are peculiar of wireless systems. Such interference occurs when a location is simultaneously reached by two transmissions. The Reduction Semantics differ on how information about the active transmissions is managed.We use the calculus to describe and analyse a few properties of a version of the Alternating Bit Protocol.     

Dataplan: An interface generator for database semantics

A model system (called DATAPLAN) is proposed for generation, access, and control of a shared database by casual users in their own terminology. The DATAPLAN system achieves this goal by planning a dialog which hierarchically defines the possible universe of discourse where casual users can communicate with the database. The plan is executed on the domains of hierarchical semantics, and controlled by pattern matching with a goal and generative backtracking mechanism. To ensure flexible and smooth communication of casual users with the shared database, the system generates individualized user class “fuzzy” interfaces. They are composed of multiplex associations of the attributes and values of the shared database with those of casual user classes in varying degrees.     

An axiomatic semantics for the synchronous language Gentzen

We propose an axiomatic semantics for the synchronous language Gentzen, which is an instantiation of the paradigm Timed Concurrent Constraint Programming proposed by Saraswat, Jagadeesan and Gupta. We view Gentzen as a prototype of the class of state-oriented synchronous languages, since it offers the basic constructs that are shared by the languages in the class. Since synchronous concurrency cannot be simulated by arbitrary interleaving, we cannot exploit “head normal forms”, on which axiomatic theories for asynchronous process calculi are based. We suggest how axiomatic semantics for other state-oriented synchronous languages can be obtained by expressing constructs of such languages in terms of Gentzen constructs.