A Formal Semantics for the SmartFrog Configuration Language

System configuration languages are now widely used to drive the deployment and evolution of large computing infrastructures. Most such languages are highly informal, making it difficult to reason about configurations, and introducing an important source of failure. We claim that a more rigorous approach to the development and specification of these languages will help to avoid these difficulties and bring a number of additional benefits. In order to test this claim, we present a formal semantics for the core of the SmartFrog configuration language. We demonstrate how this can be used to prove important properties such as termination of the compilation process. To show that this also contributes to the practical development of clear and correct compilers, we present three independent implementations, and verify their equivalence with each other, and with the semantics. Supported by an extended example from a real configuration scenario, we demonstrate how the process of developing the semantics has improved understanding of the language, highlighted problem areas, and suggested alternative interpretations. This leads us to advocate this approach for the future development of practical configuration languages.     

一种UML2的交互的形式化语义

UML2(unified modeling language2.x)的规范为其交互定义了一种基于事件发生轨迹的语义,弥补了之前版本在语义上的欠缺。但是此语义是用自然语言(英语)描述的,不够精确、不一致,并且很多细节解释得不够清楚和完备。利用集合论以组合定义的方式形式化语义,并且证明了形式化后交互的语义为拟序集,此拟序集的线性化恰好就是规范所定义的轨迹集。此形式化语义可以作为UML2交互规范的很好的补充,不但有助于UML2交互的理解,还为UML2交互的应用和研究奠定了坚实的理论基础。     

A Formal Semantics of Data Flow Diagrams

This paper presents a formal semantics of data flow diagrams as used in Structured Analysis, based on an abstract model for data flow transformations. The semantics consists of a collection of VDM functions, transforming an abstract syntax representation of a data flow diagram into an abstract syntax representation of a VDM specification. Since this transformation is executable, it becomes possible to provide a software analyst/designer with two ‘views’ of the system being modelled: a graphical view in terms of a data flow diagram, and a textual view in terms of a VDM specification. In this paper emphasis is on the motivation for the choices made in the transformation. The main aspects of the transformation itself are described using annotated VDM functions with some examples.     

SQL语言的形式语义

对SQL查询的形式语义的研究有助于形式地证明两条SQL语句是否等价,从而消除了自然语言的二义性。SQL标准对SQL的语义规则进行了定义,但是并没有很好地处理不完全信息问题。文中以中介逻辑谓词演算系统MFM为基础,构造一个形式的三值谓词演算模型EPMC,然后通过语法转化规则把SQL查询转化为EPMC,从而完整地定义了SQL查询的形式语义。     

Towards Verification of C Programs. C-Light Language and Its Formal Semantics

The C-light language is described, which is a representative subset of C. C-light permits deterministic expressions, limited use of switch and goto statements, and, instead of library functions for work with dynamic memory, includes C++ statements new and delete. A survey of structured operational semantics of the C-light language in Plotkin's style is given.     

Formal Foundations of Operational Semantics

In this paper we report on the results of a sophisticated and substantial use of PVS to establish a recent result in operational semantics. The result we establish is a context lemma for operational equivalence for very wide class of programming languages, known as the CIU theorem. The proof uses the annotated holes technique to represent contexts and compute with them. Thus this paper demonstrates that that it is possible to use PVS as a tool in the development of modern operational techniques, and a productive tool at that. The process of formalizing the CIU theorem revealed several gaps in published proof. The proof of the CIU theorem in PVS took approximately six months to develop. The actual machine checked proof involves the proving of around one thousand facts, and takes PVS slightly less than three hours of CPU time running on a Linux machine configured with 2 GBytes of main memory and four 550 MHz Xeon PIII processors.     

A Semantics for Static Type Inference in a Nondeterministic Language

Plotkin used the models of reduction in order to obtain a semantic characterization of static type inference in the pure λ-calculus. Here we apply these models to the study of a nondeterministic language, obtaining results analogous to Plotkin′s.     

KRust:Rust形式化可执行语义

Rust是新兴的系统级编程语言,旨在提供内存安全的同时保证极高的性能。Rust形式化语义是用来证明其内存安全和开发Rust程序分析工具的基础。鉴于目前没有直接描述Rust的形式化语义,提出了针对Rust语言的形式化可执行语义KRust。为了确保语义的可执行性和应用性,使用了K框架进行语义的开发。KRust目前涵盖了Rust常见的语法和语义,包括了Rust的3个核心特性:所有权、借用和生命周期。KRust通过了191个测试样例,其中157个都是来自Rust官方的测试集。语义对比测试实验发现了Rust编译器的缺陷。此外,KRust的语义还可以被应用于开发Rust程序分析工具。     

Formal Semantics of Java Expressions and Statements

Programming and Computer Software -     

构件式体系结构模型映射的形式化语义

语义一致性是模型驱动开发中模型转换正确性的一个重要标准,但目前模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题.基于软件体系结构,利用范畴理论和代数规范形式化描述体系结构模型及其间的映射关系,使之具有精确的语义.体系结构模型的形式化语义用类型范畴图表来表示,态射合成被用来追踪构件模型之间的关联和映射,不同层次模型间的映射关系用态射和函子来形式化描述.以此为基础,进一步分析了模型转换应保持的语义特性.范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪.应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动开发提供了新的认知、设计和语义计算的指导架构.     

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

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

Formal Semantics for Composite Temporal Events in Active Database Rules

A major thrust of current research in active databases focuses on allowing complex patterns of temporal events to serve as preconditions for rule triggering. Currently, there is no common formalism for specifying the semantics of composite event languages. Different systems have used an assortment of different techniques, including Finite State Automata, Petri Nets and Event Graphs. In this paper, we propose a unifying approach, based on a syntax-directed translation of composite event expressions into Datalog _1S rules, whose formal semantics defines the meaning of the original expressions. We demonstrate our method by providing a formal specification of the Event Pattern Language (EPL) developed at UCLA. This method overcomes problems and limitations affecting previous approaches and is applicable to other languages such as ODE, SNOOP and SAMOS—thus, allowing a more direct comparison across different systems.     

Recoverable Formal Language

We study the problem of recovering distorted arbitrarily long messages written in some dynamically specified formal language. We obtain necessary and sufficient conditions on the language definition for an admissible message to exist in a neighborhood of a distorted message provided that local perturbations occur rarely.

     

基于迹语义的网络安全协议形式化分析

形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段.本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约.运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证.     

一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面,并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数,即定义在上下文无关语言上的递归函数为基础,以上下文无关语言为数据类型,在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明,LFC是一个能力强、易使用的语言,适合软件形式规约获取之用,并且适合其它一些用途。     

ConSpec – A Formal Language for Policy Specification

The paper presents ConSpec, an automata based policy specification language. The language trades off clean semantics to language expressiveness; a formal semantics for the language is provided as security automata. ConSpec specifications can be used at different stages of the application lifecycle, rendering possible the formalization of various policy enforcement techniques.     

Reduction Semantics and Formal Analysis of Orc Programs

Orc is a language for orchestration of web services developed by J. Misra that offers simple, yet powerful and elegant, constructs to program sophisticated web orchestration applications. The formal semantics of Orc poses interesting challenges, because of its real-time nature and the different priorities of external and internal actions. In this paper, building upon our previous SOS semantics of Orc in rewriting logic, we present a much more efficient reduction semantics of Orc, which is provably equivalent to the SOS semantics thanks to a strong bisimulation. We view this reduction semantics as a key intermediate stage towards a future, provably correct distributed implementation of Orc, and show how it can naturally be extended to a distributed actor-like semantics. We show experiments demonstrating the much better performance of the reduction semantics when compared to the SOS semantics. Using the Maude rewriting logic language, we also illustrate how the reduction semantics can be used to endow Orc with useful formal analysis capabilities, including an LTL model checker. We illustrate these formal analysis features by means of an online auction system, which is modeled as a distributed system of actors that perform Orc computations.     

Automated Generation of Strictly Conforming Tests Based on Formal Specification of Dynamic Semantics of the Programming Language

A technique for an automated test generation for compilers, which is based on formal specifications of the programming language, is suggested. The technique makes it possible to generate tests correct from the dynamic semantics standpoint that do not depend on specific features (undefined or implementation-specific) of the semantics (the so-called strictly conforming tests). The application of the suggested technique to generating tests for C compilers is discussed in detail. For this purpose, a subset of C is defined the semantics of which, first, does not depend on the above-mentioned specific features and, second, possesses properties of type soundness and determinism, which guarantee the correct test execution for any implementation satisfying the C standard.     

遗传算法的形式化语言表示

遗传算法（Genetic Algorithm）是一类借鉴生物界的进化规律（适者生存,优胜劣汰遗传机制）演化而来的随机化搜索方法。其主要特点是直接对结构对象进行操作;具有内在的隐并行性和更好的全局寻优能力;采用概率化的寻优方法,能自动获取并指导优化的搜索空间,自适应地调整搜索方向,不需要确定的规则。如何用形式化的语言表示出遗传算法成为运用于现实的基础。文章重点讨论了遗传算法的形式化语言表示。