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.     

A temporal programming model with atomic blocks based on projection temporal logic

Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model （αPTL） which extends the projection temporal logic （PTL） to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.     

An Ontological Approach to Intelligence Gathering Using Semantic Metadata

Effectively presenting next to real-time knowledgeable answers to runtime user generated queries, from disparate sources requires the implementation of semantics to safeguard the future of knowledge discovery and reuse. The paper explores the foundations of the research for the design of an information gathering tool based on the intelligence domain; focusing on the exploration of semantic metadata, incorporating ontologies and implementing swarm intelligence theory in the conceptualisation of the system design for the IGUSMON Project, in order to present an efficient and innovative solution.     

Hybrid Bayesian estimation tree learning with discrete and fuzzy labels

Classical decision tree model is one of the classical machine learning models for its simplicity and effectiveness in applications. However, compared to the DT model, probability estimation trees （PETs） give a better estimation on class probability. In order to get a good probability estimation, we usually need large trees which are not desirable with respect to model transparency. Linguistic decision tree （LDT） is a PET model based on label semantics. Fuzzy labels are used for building the tree and each branch is associated with a probability distribution over classes. If there is no overlap between neighboring fuzzy labels, these fuzzy labels then become discrete labels and a LDT with discrete labels becomes a special case of the PET model. In this paper, two hybrid models by combining the naive Bayes classifier and PETs are proposed in order to build a model with good performance without losing too much transparency. The first model uses naive Bayes estimation given a PET, and the second model uses a set of small-sized PETs as estimators by assuming the independence between these trees. Empirical studies on discrete and fuzzy labels show that the first model outperforms the PET model at shallow depth, and the second model is equivalent to the naive Bayes and PET.     

Tagged Systems: A Framework for the Specification of History-dependent Properties

We propose a general method for the treatment of history-dependent runtime errors. When one has to control this kind of errors, a tagged version of the language is usually defined, in which tags capture only the necessary information of the history of processes. We will characterize such tagged languages as being quotients of the reachability tree defined by the computations of the original language. From this fact we can conclude that the property characterized by each tagged language is indeed a property of the original one. In this way, we can work in a common framework, instead of defining an ad hoc semantics for each property. In particular, we could still use the analysis machinery existing in the calculus in order to prove that or other related properties. We have applied this methodology to the study of resource access control in a distributed π-calculus, called Dπ. In particular, we have proved that the tagged version of Dπ is indeed a tagging according to our definition.     

Bi-inductive Structural Semantics: (Extended Abstract)

We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value λ-calculus.     

映射ELOTOS到基于FSM的性能估价模型

ELOTOS是协议描述规范语言LOTOS的扩展．本文用标号转换系统LTS（labeledtransitionsystem）给出了ELOTOS的语义．然后，通过对LTS进行踪迹等价住分析，将ELOTOS映射到基于有穷状态机FSM（finitestatemachine）的性能估价模型．     

Trace-Based Abstract Interpretation of Operational Semantics

We present trace-based abstract interpretation, a unification of severallines of research on applying Cousot-Cousot-style abstract interpretation a.i. tooperational semantics definitions (such as flowchart, big-step, and small-step semantics)that express a programs semantics as a concrete computation tree of trace paths. Aprograms trace-based a.i. is also a computation tree whose nodes contain abstractions ofstate and whose paths simulate the paths in the programs concrete computation tree.Using such computation trees, we provide a simple explanation of the central concept of collecting semantics, and we distinguish concrete from abstract collectingsemantics and state-based from path-based collecting semantics. We also expose therelationship between collecting semantics extraction and results garnered from flow-analytic and model-checking-based analysis techniques. We adapt concepts fromconcurrency theory to formalize safe and live a.i.s for computation trees; in particular, coinduction techniques help extend fundamental results to infinite computation trees.Problems specific to the various operational semantics methodologies are discussed: Big-step semantics cannot express divergence, so we employ a mixture of induction andcoinduction in response; small-step semantics generate sequences of programconfigurations unbounded in size, so we abstractly interpret source language syntax.Applications of trace-based a.i. to data-flow analysis, model checking, closure analysis,and concurrency theory are demonstrated.     

补偿通信顺序进程的扩展及失败发散语义

补偿通信顺序进程(cCSP)是通信顺序进程用于长事务建模的扩展,可用来描述服务计算中的编制程序,比如WS-BPEL程序。目前,cCSP只有操作语义和基于迹的指称语义,对死锁和发散行为的推理支持不够。本文扩展了cCSP,引入新的组合操作子,给出扩展cCSP的失败发散语义;并根据该语义,给出新引入组合操作子的重要代数规则,用于语义的理解和佐证。最后,给出一个案例描述用于展示扩展cCSP。     

Trace Semantics and Algebraic Laws for Total Store Order Memory Model

Modern multiprocessors deploy a variety of weak memory models(WMMs).Total Store Order(TSO) is a widely-used weak memory model in SPARC implementations and x86 architecture.It omits the store-load constraint by allowing each core to employ a write buffer.In this paper,we apply Unifying Theories of Programming(abbreviated as UTP) in investigating the trace semantics for TSO,acting in the denotational semantics style.A trace is expressed as a sequence of snapshots,which records the changes in registers,write buffers and the shared memory.All the valid execution results containing reorderings can be described after kicking out those that do not satisfy program order and modification order.This paper also presents a set of algebraic laws for TSO.We study the concept of head normal form,and every program can be expressed in the head normal form of the guarded choice which is able to model the execution of a program with reorderings.Then the linearizability of the TSO model is supported.Furthermore,we consider the linking between trace semantics and algebraic semantics.The linking is achieved through deriving trace semantics from algebraic semantics,and the derivation strategy under the TSO model is provided.     

Trace representation and linear complexity of binary sequences derived from Fermat quotients

We describe the trace representations of two families of binary sequences derived from the Fermat quotients modulo an odd prime p （one is the binary threshold sequences and the other is the Legendre Fermat quotient sequences） by determining the defining pairs of all binary characteristic sequences of cosets, which coincide with the sets of pre-images modulo p2 of each fixed value of Fermat quotients. From the defining pairs, we can obtain an earlier result of linear complexity for the binary threshold sequences and a new result of linear complexity for the Legendre Fermat quotient sequences under the assumption of 2p-1≠ 1 mod p2.     

Fully abstract trace semantics for protected module architectures

Protected module architectures (PMAs) are isolation mechanisms of emerging processors that provide security building blocks for modern software systems. Reasoning about these building blocks means reasoning about elaborate assembly code, which can be very complex due to the loose structure of the code. One way to overcome this complexity is providing the code with a well-structured semantics. This paper presents one such semantics, namely a fully abstract trace semantics, for an assembly language enhanced with PMA. The trace semantics represents the behaviour of protected assembly code with simple abstractions, unburdened by low-level details, at the maximum degree of precision. Furthermore, it captures the capabilities of attackers to protected code and simplifies the formulation of a secure compiler targeting PMA-enhanced assembly language.     

Generic Trace Theory

Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism” such as classical non-determinism (with a set of possible choices) vs. probabilistic non-determinism. In this paper we claim that these various forms of “trace semantics” are instances of a single categorical construction, namely coinduction in a Kleisli category. This claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in the work of Smyth and Plotkin.     

时间Petri网弱语义模型的形式化分析

时间Petri网存在强语义和弱语义两种模型,弱语义模型更适合建模和分析外部环境触发的冲突选择问题,但其形式语义和可达性分析方面的研究,却很少有人问津。利用带标号的变迁系统定义时间Petri网弱语义模型的形式语义,采用时间戳状态类方法分析它的可达性,并证明了可达性问题的可判性和状态类时间戳的全局时间性质。     

There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations

It is well known that for many non-deterministic programming languages there is no continuous fully abstract fixpoint semantics. This is usually attributed to “problems with continuity”, that is, the assumption that the semantic functions should be continuous supposedly plays a role in the difficulties of giving a fully abstract fixpoint semantics. We show that for a large class of non-deterministic programming languages there is no fully abstract least fixpoint semantics even if one considers arbitrary functions (not necessarily continuous) over arbitrary partial orders (not necessarily complete).     

基于安全进程代数的非演绎安全模型的分析与验证

就刻画安全的性质而言,基于非演绎信息流的安全模型较基于访问控制的安全模型更为确切和本质。在基于迹语义对非演绎信息流安全模型进行分析的基础上,基于安全进程代数给出非演绎模型的形式化描述,然后基于系统的安全进程代数表达式给出非演绎模型的验证算法且开发了相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。     

基于结构模型的人运动图像语义描述

人运动图像语义的研究是对人运动图像中人体运动行为的一种描述方法,通过其语义来实现图像的识别与检索。该文希望通过对人体运动的几种较为简单的动作语义的研究,来开启对人运动图像语义的全面研究。为了实现该目标,提出了基于模型的人运动图像的语义描述,即模型语义,模型语义具有直观性、推导性和可行性。通过定义基本模型和语义操作规则,建立一个语义的形式描述理论,此模型语义是人运动图像语义全面研究的基础。     

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     

图像语义的模型结构描述

图像语义是研究图像模式识别与图像检索的一个新理论。如何有效地建立起图像语义的描述,图像的语义模型能够给出一个直观的、形象的描述,为研究图像语义奠定快速的、可靠的基础。文章从图像固有属性、图像对象和人为意识三方面就图像语义的模型作了一些探讨性研究,为进一步研究图像语义的描述奠定了基础。     

A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries

Backward compatibility is the property that an old version of a library can safely be replaced by a new version without breaking existing clients. Formal reasoning about backward compatibility requires an adequate semantic model to compare the behavior of two library implementations. In the object-oriented setting with inheritance and callbacks, such a model must account for the complex interface between library implementations and clients.In this paper, we develop a fully abstract trace-based semantics for class libraries in object-oriented languages, in particular for Java-like sealed packages. Our approach enhances a standard operational semantics such that the change of control between the library and the client context is made explicit in terms of interaction labels. By using traces over these labels, we abstract from the data representation in the heap, support class hiding, and provide fully abstract package denotations. Soundness and completeness of the trace semantics is proven using specialized simulation relations on the enhanced operational semantics. The simulation relations also provide a proof method for reasoning about backward compatibility.