A Standard Model-Theoretic Approach to Operational Semantics of Recursive Programs

In this paper we try to introduce a new approach to operational semantics of recursive programs by using ideas in the“priority method”which is a fundamental tool in Recursion Theory.In lieu of modelling partial functions by introducing undefined values in a traditional approach,we shall define a priority derivation tree for every term,and by respecting the rule“attacking the subterm of the highest priority first”we define transition relations,computation sequences etc.directly based on a standard interpretation which includes no undefined value in its domain.Finally,we prove that our new approach generates the same operational semantics as the traditional one.It is also pointed out that we can use our strategy to refute a claim of Loeckx and Sieber that the opperational semantics of recursive programs cannot be built based on predicate logic.

Operational Semantic of Workflow Engine and the Realizing Technique

At present, there is no formalized description of the executing procedure of workflow models. The procedure of workflow models executing in workflow engine is described using operational semantic. The formalized description of process instances and activity instances leads to very clear structure of the workflow engine, has easy cooperation of the heterogeneous workflow engines and guides the realization of the workflow engine function. Meanwhile, the software of work flow engine has been completed by means of the formalized description.

Real-time collaborative design based on operation semantics in distributed CAD environment

This paper proposes a collaborative design model based on operation semantics in a distributed computer-aided design (CAD) environment. The goal is to reduce time consumption in data format conversion and the requirement of network bandwidth so as to improve the cooperative ability and the synchronization efficiency. Firstly, real-time collaborative design is reviewed and three kinds of real-time collaborative design models are discussed. Secondly, the concept of operation semantics is defined and the framework of an operation semantics model is presented. The operation semantics carries the original design data and actual operation process to express design intent and operation activity in conventional CAD systems. Finally, according to the operation semantics model, a CAD operation primitive is defined which can be retrieved from and mapped to the local CAD system operation commands; a distributed CAD collaborative architecture based on the model is presented, and an example is given to verify the model.

Ontology-Based Semantic Multi-agent Framework for Micro-grids with Cyber Physical Concept

The distributed hierarchical control based on multi-agent system(MAS) is the main control method of micro-grids.By allowing more flexible interactions between computing components and their physical environments,cyber physical system(CPS) presents a new approach for the distributed hierarchical engineering system,with micro-grids included.The object of this paper is to integrate the CPS concept with MAS technology and propose a new control framework for micro-grids.With the analysis of the operating mode and control method of micro-grids,the cyber physical control concepts of ontologybased semantic agent are discussed.Then an MAS-based architecture of cyber physical micro-grid system and an intelligent electronic device(IED) function structure are proposed.Finally,in order to operate and test the cyber physical micro-grid concept,an integrated simulation model is presented.

Geometry Services Construction Based on Ontology towards Cooperative Design in Cloud Environment

APIs of CAD system could be encapsulated to construct web services so as to provide standard access interfaces for web-based cooperative design. However, lack of semantic supporting make integration of heterogeneous modelling system limited to operational level. On the purpose of carrying out cooperative design in a flexible cloud environment, an intelligent and effective support mechanism is needed for mass and complex interaction in cooperative work. Therefore, Ontology-based Geometry Modeling Services Environment （OGMSE） is provided to realize a knowledge-level geometry modeling so as to supported semantic 3D model management and intelligent operation support. First, CAD APIs are encapsulated into web service for web invocation. Then, ontology contained structural semantic and operational semantic is built for management of models and modeling process. Lastly, conception-driven modeling mechanism is built to invocate service according to interaction requirement, thus to realize conception-level cooperative design. Based on an open geometry engine, a prototype system has been developed. The result shows that the approach provides a reference direction for large-scale application on the network.

Semantic theories of programs with nested interrupts

In the design of dependable software for embed- ded and real-time operating systems, time analysis is a cru- cial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a pro- gramming language to describe programs with interrupts that is comprised of two essential parts： main program and inter- rupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the mean- ings of our language. Furthermore, a strategy of deriving de- notational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational se- mantics by showing the consistency between the derived de- notational semantics and the original denotational semantics.

Mechanized semantics and refinement of UML-Statecharts

The Unified Modeling Language （UML） is an industry standard for modeling analysis and design. However, the semantics of UML is not precisely defined and the correctness of refinement relations cannot be verified. In this study, we use the theorem proof assistant Coq to formalize and mechanize the semantics of UML- Statecharts and the refinement relations between models. Based on the mechanized semantics, the desired properties of both the semantics and the refinement relations can be described and proven as predicates and lemmas. This approach provides a promising way to obtain certified fault-free modeling and refinement.

Design and Implementation of Spacecraft Automatic Test Language

Spacecraft automatic test system, a comprehensive spacecraft test information system based on the various spacecraft test specifications formalized as spacecraft test language, is an important means to improve test efficiency. With the new require- ments of the multi-spacecraft test in China, the study of the spacecraft test language becomes a new challenge for spacecraft test field. In this article, a high-order spacecraft test language, China aerospace test and operation language （CATOL）, is given asso- ciated with the current test requirements; meanwhile, the structure of the language is presented. Then, for characterizing and formalizing the spacecraft processes, the syntax and operational semantics of one of the sub-languages, CATOL-PR, are defined. Finally, the prototype system of this proposed language is presented. This language will improve the specification of spacecraft test work in China and the efficiency of spacecraft testers, and promote the development in spacecraft automatic test.

EtherClue:Digital investigation of attacks on Ethereum smart contracts

Programming errors in Ethereum smart contracts can result in catastrophic financial losses from stolen cryptocurrency.While vulnerability detectors can prevent vulnerable contracts from being deployed,this does not mean that such contracts will not be deployed.Once a vulnerable contract is instantiated on the blockchain and becomes the target of attacks,the identification of exploit transactions becomes indispensable in assessing whether it has been actually exploited and identifying which malicious or subverted accounts were involved.In this work,we study the problem of post-factum investigation of Ethereum attacks using Indicators of Compromise(IoC)specially crafted for use in the blockchain.IoC definitions need to capture the side-effects of successful exploitation in the context of the Ethereum blockchain.Therefore,we define a model for smart contract execution,comprising multiple abstraction levels that mirror the multiple views of code execution on a blockchain.Subsequently,we compare IoCs defined across the different levels in terms of their effectiveness and practicality through EtherClue,a prototype tool for investigating Ethereum security incidents.Our results illustrate that coarse-grained IoCs defined over blocks of transactions can detect exploit transactions with less computation.However,they are contract-specific and suffer from false negatives.On the other hand,fine-grained IoCs defined over virtual machine instructions can avoid these pitfalls at the expense of increased computation,which is nevertheless applicable for practical use.

View Creation for Queriesin Object Oriented Databases

A view in object oriented databases corresponds to virtual schemawith restructured generalization and decomposition hierarchies. Numbers of viewcreation methodologies have been proposed. A major drawback of existing method-ologies is that they do not maintain the closure property. That is, the result of aquery does not have the same semantics as embodied in the object oriented datamodel. Therefore, this paper presents a view creation methodology that derives aclass in response to a user's query, integrates derived class in global schema (i.e.,considers the problem of classes moving in class hierarchy) and selects the requiredclasses from global schema to create the view for user's query. Novel idea of viewcreation includes: (a) an object algebra for class derivation and customization (wherethe derived classes in terms of object instances and procedure/methods are studied),(b) maintenance of closure property, and (c) classification algorithm which providesmechanism to deal with the problem of a class moving in a class hierarchy.