A Formal Semantics for DAI Language NUML

1IntroductionAsE.H.Durfeestatesin[1]:Artificia1Inte1ligence(AI)hasemphasizedbuilding"stand-alonesystems"thatcansolveproblemswithminimalhelpfromothersystems(computerorman).Thesesystemshavetraditionallybeenbrittle,inthesensethattheyfailmiser-ablywhenpresentedwithproblemsevens1ightlyoutsideoftheir1imitedrangeofexpertise...Amorepowerful,extensiblestrategyforovercomingtheinherentboundsofintelligencepresentinanyfilliteAI(ornaturaI)systemistoputsysteminasocietyofsystems,sothatitcandrawonadiversec…     

A comparative study of two formal semantics of the SIGNAL language

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. There exist several semantics for SIG- NAL, such as denotational semantics based on traces （called trace semantics）, denotational semantics based on tags （called tagged model semantics）, operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by syn- chronous transition systems （STS）, etc. However, there is lit- tle research about the equivalence between these semantics. In this work, we would like to prove the equivalence be- tween the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different defini- tions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The dis- tance between these two semantics discourages a direct proof of equivalence. Instead, we transform them to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.     

A comparative study of two formal semantics of the SIGNAL language

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics), denotational semantics based on tags (called tagged model semantics), operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by synchronous transition systems (STS), etc. However, there is little research about the equivalence between these semantics. In this work, we would like to prove the equivalence between the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different definitions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The distance between these two semantics discourages a direct proof of equivalence. Instead, we transformthem to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.     

Nivel: a metamodelling language with a formal semantics

Much work has been done to clarify the notion of metamodelling and new ideas, such as strict metamodelling, distinction between ontological and linguistic instantiation, unified modelling elements and deep instantiation, have been introduced. However, many of these ideas have not yet been fully developed and integrated into modelling languages with (concrete) syntax, rigorous semantics and tool support. Consequently, applying these ideas in practice and reasoning about their meaning is difficult, if not impossible. In this paper, we strive to add semantic rigour and conceptual clarity to metamodelling through the introduction of Nivel, a novel metamodelling language capable of expressing models spanning an arbitrary number of levels. Nivel is based on a core set of conceptual modelling concepts: class, generalisation, instantiation, attribute, value and association. Nivel adheres to a form of strict metamodelling and supports deep instantiation of classes, associations and attributes. A formal semantics is given for Nivel by translation to weight constraint rule language (WCRL), which enables decidable, automated reasoning about Nivel. The modelling facilities of Nivel and the utility of the formalisation are demonstrated in a case study on feature modelling.

A formal semantics for an active functional DBPL

We describe how the functional database programming language PFL is extended with an active component without compromising either its declarative semantics or its syntax. We give a formal specification of the active component using PFL itself, including event specification and detection, parameter-binding, reaction scheduling and abort handling. We describe how a user-specified function can be cast as a primitive event, and discuss the expressiveness of events and the optimisation of event detection.     

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.     

Describing process plans as the formal semantics of a language of shape

A method of formalising manufacturing information for use in the design process is presented. The method uses a grammar of shape and its formal semantics to describe the set of objects manufacturable by a given process, to generate objects from that set, and to describe corresponding process plans for the manufacture of those objects. The grammar thus defines a search space for generative process planning, and the semantics provide an interpretation of the results of a search in that space.     

A formal semantics for the Taverna 2 workflow model

This paper presents a formal semantics for the Taverna 2 scientific workflow system. Taverna 2 is a successor to Taverna, an open-source workflow system broadly adopted within the e-science community worldwide. The new version improves upon the existing model in two main ways: (i) by adding support for data pipelining, which in turns enables input streams of indefinite length to be processed efficiently; and (ii) by providing new extensibility points that make it possible to add new operators to the workflow model. Consistent with previous work by some of the authors, we use trace semantics to describe the effect of workflow computations, and we show how they can be used to describe the new features in the Taverna 2 model.     

A formal semantics for concurrent systems with a priority relation

Summary A formal semantics for the COSY path expressions with a priority relation is proposed. It turns out that in the general case the full aspects of behaviours of systems specified by such expressions cannot be modeled by vector firing sequences (a standard semantics for the case without priorities), although vector firing sequences (but without interpretation as causality relations) can correctly be extended for expressions with priorities, and some (but not all) aspects of behaviours, like deadlockfreeness and adaquacy properties, can be defined in terms of vector firing sequences. To describe the behaviours of the COSY priority path expressions entirely, a new semantics, called the multiple firing sequence semantics, is introduced and some its properties are proved.Main part of this work was done during the author's visit at the Institute of Electronic Systems, Aalborg University Centre, Aalborg, DenmarkOn leave from the Warsaw Technical University, Poland     

A formal semantics for debugging synchronous message passing-based concurrent programs

During a human-exoskeleton collaboration, the interaction torque on exoskeleton resulting from the human cannot be clearly determined and conducted by normal physical models. This is because the torque depends not only on direction and orientation of both human-operator and exoskeleton but also on the physical properties of each operator. In this paper, we present our investigations on the relationship between the interaction torques with the dynamic factors of the human-exoskeleton systems using state-of-the-art learning techniques （nonparametric regression techniques） and provide control applications based on the findings. Exper- imental data was collected from various human-operators when they were attached to the designed exoskeleton to perform unconstraint motions with and without control. The results showed that regardless of how the ex- periments were done and which learning method was chosen, the resulting interaction could be best represented by time varying non-linear mappings of the operator＇s angular position, and the exoskeleton＇s angular position, velocity, and acceleration during locomotion. This finding has been applied to advanced controls of the lower exoskeletal robots in order to improve their performance while interacting with human.     

A formal semantics for debugging synchronous message passing-based concurrent programs

In this paper, we propose a semantic framework to debug synchronous message passing-based con- current programs, which are increasingly useful as parallel computing and distributed systems become more and more pervasive. We first design a concurrent programming language model to uniformly represent exist- ing concurrent programming languages. Compared to sequential programming languages, this model contains communication statements, i.e., sending and receiving statements, and a concurrent structure to represent com- munication and concurrency. We then propose a debugging process consisting of a tracing and a locating procedure. The tracing procedure re-executes a program with a failed test case and uses specially designed data structures to collect useful execution information for locating bugs. We provide for the tracing procedure a struc- tural operational semantics to represent synchronous communication and concurrency. The locating procedure backward locates the ill-designed statement by using information obtained in the tracing procedure, generates a fix equation, and tries to fix the bug by solving the fix equation. We also propose a structural operational semantics for the locating procedure. We supply two examples to test our proposed operational semantics.     

A layered semantics for a parallel object-oriented language

We develop a denotational semantics for POOL, a parallel object-oriented programming language. The main contribution of this semantics is an accurate mathematical model of the most important concept in object-oriented programming: the object. This is achieved by structuring the semantics in layers working at three different levels: for statements, objects and programs. For each of these levels we define a specialized mathematical domain of processes, which we use to assign a meaning to each language construct. This is done in the mathematical framework of complete metric spaces. We also define operators that translate between these domains. At the program level we give a precise definition of the observable input/output behaviour of a particular program, which could be used at a later stage to decide the issue of full abstractness. We illustrate our semantic techniques by first applying them to a toy language similar to CSP.This paper describes work done in ESPRIT Basic Research Action 3020,Integration.     

Comments on “A formal semantics for object modeldiagrams”

The author indicates some things that need clarifying in the paper cited in the title. The paper does not make it clear that a class of objects is not equivalent to a set of tuples. In a set of tuples two different tuples cannot contain the same data. Two different objects in a given class can contain the same data. In most of the paper this does not matter. However, the simulation function between a subclass and a superclass must be injective, but the (overloaded) simulation function between the sets of tuples usually cannot be injective     

Computability concepts for programming language semantics

This paper is about mathematical problems in programming language semantics and their influence on recursive function theory. We define a notion of computability on continuous higher types (for all types) and show its equivalence to effective operators. This resuit shows that our computable operators can model mathematically (i.e. extensionally) everything that can be done in an operational semantics. These new recursion theoretic concepts which are appropriate to semantics also allow us to construct Scott models for the λ-calculus which contain all and only computably elements. Depending on the choice of the initial cpo, our general theory yields a theory for either strictly determinate or else arbitrary non-deterministic objects (parallelism). The formal theory is developed in Part II of this paper. Part I gives motivation and comparison with related work.     

Equivalence of formal semantics definition methods

There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves.Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.A full version of this paper can be accessed via our web page http://www.cs.man.ac.uk/fmethods/ facj.html     

The formal specification of ORN semantics

Object Relationship Notation (ORN) is a declarative scheme that permits a variety of common types of relationships to be conveniently defined to a Database Management System (DBMS), thereby allowing the DBMS to automatically enforce their semantics. Though first proposed for object DBMSs, ORN is applicable to any data model that represents binary entity-relationships or to any DBMS that implements them. In this paper, we first describe ORN semantics informally as has been done in previous papers. We then provide a formal specification of these semantics using the Z-notation. Specifying ORN semantics via formal methods gives ORN a solid mathematical foundation. The semantics are defined in the context of an abstract database of sets and relations in a recursive manner that is precise, unambiguous, and noncircular.