SPARE: a development environment for program analysis algorithms

A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature of the specifications eases the derivation of formal proofs of correctness for the analysis algorithm. SPARE (structured program analysis refinement environment) is based on a hybrid approach that combines the positive aspects of both the operational and the semantics-driven approach. An extended denotational framework is used to provide specifications in a modular fashion. Several extensions to the traditional denotational specification language have been designed to allow analysis algorithms to be expressed in a clear and concise fashion. This extended framework eases the design of analysis algorithms as well as the derivation of correctness proofs. The tool provides automatic implementation for testing purposes     

Formalizing and testing the consistency of DSL transformations

A domain specific language (DSL) focuses on the essential concepts in a specific problem domain, and abstracts from low-level implementation details. The development of DSLs usually centers around the meta-model, grammar and code generator, possibly extended with transformations to analysis models. Typically, little attention is given to the formal semantics of the language, whereas this is essential for reasoning about DSL models, and for assessing the correctness of the generated code and analysis models. We argue that the semantics of a DSL should be defined explicitly and independently of any code generator, to avoid all kinds of complexities from low-level implementation details. As the generated analysis models must reflect some of these implementation details, we propose to formalize them separately. To assess the correctness and consistency of the generated code and analysis models in a practical way, we use conformance testing. We extensively illustrate this general approach using specific formalizations for an industrial DSL on collision prevention. We do not aim for a generic semantic model for any DSL, but this specific DSL indicates the potential of a modular semantics to facilitate reuse among DSLs.     

Neverlang: A framework for feature-oriented language development

Reuse in programming language development is an open research problem. Many authors have proposed frameworks for modular language development. These frameworks focus on maximizing code reuse, providing primitives for componentizing language implementations. There is also an open debate on combining feature-orientation with modular language development. Feature-oriented programming is a vision of computer programming in which features can be implemented separately, and then combined to build a variety of software products. However, even though feature-orientation and modular programming are strongly connected, modular language development frameworks are not usually meant primarily for feature-oriented language definition. In this paper we present a model of language development that puts feature implementation at the center, and describe its implementation in the Neverlang framework. The model has been evaluated through several languages implementations: in this paper, a state machine language is used as a means of comparison with other frameworks, and a JavaScript interpreter implementation is used to further illustrate the benefits that our model provides.     

工作流系统中的业务过程描述及分析

过程模型是业务过程的形式化定义,它的正确性直接影响业务目标的实现。定义了一种过程描述语言并对使用这种语言描述的过程模型进行分析,之后给出了工作流执行的控制算法。     

Java-MaC: A Run-Time Assurance Approach for Java Programs

We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance that the target program is running correctly with respect to a formal requirements specification by monitoring and checking the execution of the target program at run-time. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which does not provide formal guarantees about the correctness of the system.Use of formal requirement specifications in run-time monitoring and checking is the salient aspect of the MaC architecture. MaC is a lightweight formal method solution which works as a viable complement to the current heavyweight formal methods. In addition, analysis processes of the architecture including instrumentation of the target program, monitoring, and checking are performed fully automatically without human direction, which increases the accuracy of the analysis. Another important feature of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors, which allows the reuse of a high-level requirement specification even when the target program implementation changes. Furthermore, this separation makes the architecture modular and allows the flexibility of incorporating third party tools into the architecture. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.     

An on-the-fly grammar modification mechanism for composing and defining extensible languages

Adaptable Parsing Expression Grammar (APEG) is a formal method for defining the syntax of programming languages. It provides an on-the-fly mechanism to perform modifications of the syntax of the language during parsing time. The primary goal of this dynamic mechanism is the formal specification and the automatic parser generation for extensible languages. In this paper, we show how APEG can be used for the definition of the extensible languages SugarJ and Fortress, clarifying many aspects of the syntax of these languages. We also show that the mechanism for on-the-fly modification of syntax rules can be useful for defining grammars in a modular way, implementing almost all types of language composition in the context of specification of extensible languages.     

Two Congruent Semantics for Prolog with CUT

The development of a formal semantics for a given programming language can proceed in several stages,At each stage we give an alternative semantic definition of the language,and each definition embodies successively more and more implementation details.Then we formulate and prove at each stage the congruence conditions between successive definitions in the sequence.This paper presents two formal semantics for Prolog with “cut” and shows the congruence condition between them.     

Automated testing of DSL implementations—experiences from building mbeddr

Domain-specific languages promise to improve productivity and quality of software development by providing problem-adequate abstractions to developers. Projectional language workbenches, in turn, allow the definition of modular and extensible domain specific languages, generators, and development environments. While recent advances in language engineering have enabled the definition of DSLs and tooling in a modular and cost-effective way, the quality assurance of their implementation is still challenging. In this paper, we discuss our work on testing different aspects of the implementation of domain specific languages and associated tools, and present several approaches to increase the automation of language testing. We illustrate these approaches with the Jetbrains MPS language workbench and our experience with testing mbeddr, a set of domain specific languages and tools on top of C tailored to embedded software development. Based on the experience gained from the mbeddr project, we extract generic lessons for practitioners as well as challenges which need more research.     

Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL

This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.     

Deriving a compiler from an operational semantics written in VDL

This paper addresses the issue of compiler correctness. The approach taken is to systematically construct a correct compiler for a language from a formal semantic definition of the language. For this purpose, an operational semantics of a language is chosen as the basis for the approach. That is, the compiler for a language is derived from an interpreter of the language. The derivation process uses the notion of mixed computation proposed by Ershov. Briefly stated, one begins interpreting and when a primitive state changing instruction is about to be executed, the instruction is emitted as code instead. The correctness of all compilers produced by the method is guaranteed by proving the derivation rules correct. This proof is a one-time task for each specification language. The specification language studied in this paper is the Vienna Definition Language (VDL). The object code generated by the compiler is in an intermediate language close to an assembly language. Therefore, the translation from the intermediate language into the assembly language should be straightforward.     

一种基于模块单子语义的动态程序切片方法

提出一种基于程序模块单子语义的新动态切片方法--模块单子动态切片.首先通过单子转换器,将切片这一类计算抽象成独立于具体语言的实体：切片单子转换器.然后,将该切片转换器作为模块加载到实际程序中,并给出相应的模块单子动态切片算法.据此,可直接在抽象语法结构上计算动态切片,不必记录程序执行历史;相应单子切片器也无需显式地构造诸如依赖图的中间结构.这种模块化抽象机制使得文中的动态切片算法具有很强的可扩展性和重用性.     

Bridging the gap between formal semantics and implementation of triple graph grammars

The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches, it is usually not really clear under which constraints particular implementations really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. While the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria, and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static and runtime checks can be employed to guarantee these criteria.     

A verification approach to applied system security

We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.     

FP──VLSI自动综合系统

ＦＰ—ＶＬＳＩ自动综合系统是一个集成化的ＶＬＳＩ自动设计工具，它能完成从并行算法到脉动算法到脉动结构再到逻辑结构最后到ＣＭＯＳ版图的自动综合过程．ＦＰ—ＶＬＳＩ系统以脉动阵列为ＶＬＳＩ的体系结构，采用具有良好代数性质的ＦＰ／Ｂ语言作为各层次的描述语言，通过程序变换进行综合和优化．该系统支持形式化的ＶＬＳＩ设计方法，能保证设计结果的正确性．     

Combining Deep and Shallow Embeddings

This paper presents an approach for verifying translator correctness when the source language has formal semantics. Instead of verifying the translator implementation, a novel language mechanization combination is devised to reduce total complexity involved. A deep embedding is defined to serve as a baseline for specification meaning. For each specification, an equivalence proof is constructed and conducted to ensure that the translated shallow representation is semantically equivalent to the deep representation. Structure of an equivalence proof is systematic and can be derived from specification structure mechanically. The use of two embeddings also affects the embeddings favourably by enabling them to be defined in a simpler manner.