Java-MaC: A Run-time Assurance Tool 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 about the correct execution of target programs at run-time. Monitoring and checking is performed based on a formal specification of system requirements. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which only partially validates an implementation. Java-MaC provides a lightweight formal method solution as a viable complement to the current heavyweight formal methods. An important aspect of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors against a formal requirements specification. Another salient feature is automatic instrumentation of executable codes. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.     

Monitoring, Checking, and Steering of Real-Time Systems

The MaC system has been developed to provide assurance that a target program is running correctly with respect to formal requirements specification. This is achieved 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 only partially validates an implementation. One weakness of the MaC system is that it can detect property violations but cannot provide any feedback to the running system. To remedy this weakness, the MaC system has been extended with a feedback capability. The resulting system is called MaCS (Monitoring and Checking with Steering). The feedback component uses the information collected during monitoring and checking to steer the application back to a safe state after an error occurs. We present a case study where MaCS is used in a control system that keeps an inverted pendulum upright. MaCS detects faults in controllers and performs dynamic reconfiguration of the control system using steering.     

Computational Analysis of Run-time Monitoring: Fundamentals of Java-MaC

A run-time monitor shares computational resources, such as memory and CPU time, with the target program. Furthermore, heavy computation performed by a monitor for checking target program's execution with respect to requirement properties can be a bottleneck to the target program's execution. Therefore, computational characteristics of run-time monitoring cause a significant impact on the target program's execution.We investigate computational issues on run-time monitoring. The first issue is the power of run-time monitoring. In other words, we study the class of properties run-time monitoring can evaluate. The second issue is computational complexity of evaluating properties written in process algebraic language. Third, we discuss sound abstraction of the target program's execution, which does not change the result of property evaluation. This abstraction can be used as a technique to reduce monitoring overhead. Theoretical understanding obtained from these issues affects the implementation of Java-MaC, a toolset for the run-time monitoring and checking of Java programs. Finally, we demonstrate the abstraction-based overhead reduction technique implemented in Java-MaC through a case study.     

Requirements for a Practical Network Event Recognition Language

We propose a run-time monitoring and checking architecture for network protocols called Network Event Recognition. Our framework is based on passively monitoring the packet trace produced by a protocol implementation and checking it for properties written in a formal specification language, NERL. In this paper, we describe the design requirements for NERL. We show how the unique requirements of network protocol monitoring impact design and implementation options. Finally we outline our prototype implementation of NERL and discuss two case studies: checking the correctness of network protocol simulations and privacy issues in packet-mode surveillance.     

Formalizing Java-MaC

The Java-MaC framework is a run-time verification system for Java programs that can be used to dynamically test and enforce safety policies. This paper presents a formal model of the Java-MaC safety properties in terms of an operational semantics for Middleweight Java, a realistic subset of full Java. This model is intended to be used as a framework for studying the correctness of Java-MaC program instrumentation, optimizations, and future experimentation with run-time monitor expressiveness. As a preliminary demonstration of this model's applicability for these tasks, the paper sketches a correctness result for a simple program instrumentation scheme.     

A Type System for the Java Bytecode Language and Verifier

The Java Virtual Machine executes bytecode programs that may have been sent from other, possibly untrusted, locations on the network. Since the transmitted code may be written by a malicious party or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier to check the code for type errors before it is run. As illustrated by reported attacks on Java run-time systems, the verifier is essential for system security. However, no formal specification of the bytecode verifier exists in the Java Virtual Machine Specification published by Sun. In this paper, we develop such a specification in the form of a type system for a subset of the bytecode language. The subset includes classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. We also present a type checking algorithm and prototype bytecode verifier implementation, and we conclude by discussing other applications of this work. For example, we show how to extend our formal system to check other program properties, such as the correct use of object locks. This revised version was published online in August 2006 with corrections to the Cover Date.     

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.     

Software monitoring through formal specification animation

This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs.     

Concurrent runtime monitoring of formally specified programs

A methodology for continuously monitoring a program for specification consistency during program execution is described. Prior development of the formal specification and program is assumed. The program is annotated with constructs from a formal specification language, and the formal specification constructs are transformed into checking code, which is then inserted into the underlying program. Calls to this checking code are inserted into underlying program wherever it can potentially become inconsistent with its specification. If an inconsistency does in fact occur, diagnostic information is provided. The implementation of such a system for Anna (annotated Ada) subtype annotations is presented     

Linking simulation with formal verification at a higher level

We use simulation to bridge the gap between specification and formal verification of high-level models and simulation of RTL models. The authors apply their practical, two-phase procedure for defining the refinement map to the Alpha 21364 multiprocessing hardware. The methodology and tools they present can improve simulation coverage. Our technique verifies that a hardware design described at the RTL is a correct implementation of an algorithm-level, executable formal specification. We use a high-level formal specification as the basis for monitoring functional correctness, measuring simulation coverage, and generating test cases.     

基于程序运行形式化分析的软件故障监控技术

关键软件要求极高的可靠性和安全性,然而当前的技术途径尚不能完全消除软件故障——软件测试不能保证软件正确性,模型检查等形式化验证技术也存在着诸多局限。文章提出了基于监控程序运行途径来捕获软件故障和验证程序性质正确性,构建了基于程序运行形式化分析的软件故障监控（SFMRFA）模型,在监控逻辑表达、程序插桩、multi-agent设计等关键技术的基础上开发计算机辅助工具来监控、分析和引导程序执行,使软件运行当中可测、可控,避免软件失效。     

Application of a transformational software development methodology to VLSI design

Like software development, VLSI design can be modeled as a series of transformations leading from a high-level formal specification to a concrete implementation. Automating such transformations offers a way to improve the correctness of the design process while reducing its cost. This paper addresses the portion of the design process that converts abstract algorithms into functional-level circuits (collections of primitive computational elements and their interconnections). By defining an isomorphism between such circuits and a restricted subset of programs, we can use source-to-source program transformations to map algorithms into circuits. The paper presents example transformations for allocating operations to components, making communication paths explicit, and designing sequential control mechanisms. A prototype implementation has successfully rederived much of the design of a published VLSI graphics display processor.     

A framework for the design and automated implementation of communication aspects in multi-agent systems

This paper presents REFCON, a framework for the automated development of Agent Communication Contexts (ACCs) in multi-agent systems (MASs). ACCs are intended to capture the interaction requirements of a MAS.A formal specification framework is first presented, aimed at modelling an ACC as a set of rules for filtering and filling messages, based on their contents, and the names and roles of the exchanging agents. A XML-based specification language is then introduced, which encodes the specification formalism for the sake of its computer processing. Finally, an object-oriented software architecture capable of supporting ACC-based MAS development is presented.REFCON key characteristic is that it allows a seamless integration of ACC support (even) into an existing MAS, at run-time, independently of the agent platform used for the implementation. This is made possible by a layered software architecture based on computational reflection, a technology that allows transparent evolution and adaptation of existing systems. The REFCON framework is also dynamic, in the two-fold sense that it is capable of both adding new rules and handling multiple contexts, which it can easily switch among, at run-time. The ACC-based design of an example MAS for document sharing is briefly discussed, as a demonstration of the principles put forward.     

Correct transformation: From object-based graph grammars to PROMELA

Model transformation is an approach that, among other advantages, enables the reuse of existing analysis and implementation techniques, languages and tools. The area of formal verification makes wide use of model transformation because the cost of constructing efficient model checkers is extremely high. There are various examples of translations from specification and programming languages to the input languages of prominent model checking tools, like SPIN. However, this approach provides a safe analysis method only if there is a guarantee that the transformation process preserves the semantics of the original specification/program, that is, that the transformation is correct. Depending on the source and/or target languages, this notion of correctness is not easy to achieve. In this paper, we tackle this problem in the context of Object-Based Graph Grammars (OBGG). OBGG is a formal language suitable for the specification of distributed systems, with a variety of tools and techniques centered around the transformation of OBGG models. We describe in details the model transformation from OBGG models to PROMELA, the input language of the SPIN model checker. Amongst the contributions of this paper are: (a) the correctness proof of the transformation from OBGG models to PROMELA; (b) a generalization of this process in steps that may be used as a guide to prove the correctness of transformations from different specification/programming languages to PROMELA.     

Language extensions for specifying program access control policies in programming languages

The scope rules in programming languages control the sharing of data among program units, e.g., blocks and procedures. Typically, scope rules provide an all-or-nothing kind of access control. A wide range of programming problems exist which require finer access control as well as considerable sophistication for the implementation of access control policies on high-level data objects such as files. This paper presents a number of language extensions that permit the programmer to specify the degree of access control for each abstract object that a program can manipulate. The number of extensions has been kept as small as possible, while allowing the user to specify conveniently the access control policies that he desires. Some of the extensions permit access policies to be specified such that access correctness can be completely determined at compile time; other extensions permit policies to be specified that require some access checking to be done at run-time in order to ensure access correctness.     

Visual Specification of Systems with Heterogeneous Coordination Models

In this paper a prototype of a visual specification language called Visual Coordination Diagrams (VCD) for high-level design of concurrent systems with heterogeneous coordination models is presented. The key property of VCD is the separation of behavioral aspects from coordination aspects. We also highlight the heterogeneity of VCD which has two levels. At first, it allows different coordination models to be mixed in a particular specification. Secondly, different formalisms can be incorporated to VCD for specification of behavioral aspects. This paper contains an overview of the language followed with its formal definition. An example of using the language is also given.     

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     

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.     

Game-theoretic simulation checking tool

Model checking is one of the most commonly used methods for checking program correctness. In this method, one verifies a program model given by the Kripke structure (labeled transition system) rather than the program itself. The specification is usually given as a temporal logic formula. In many subtasks of model checking, it is necessary to use relations that are defined on the set of program models and preserve the satisfiability of temporal logic formulas. There exist many relations of this kind, which are called simulation relations. In the present paper, we introduce a tool designed to check a wide class of simulation relations between finite models of programs. This tool is based on the simulation checking game-theoretic approach. The tool consists of two components. The first component is the formal language, which allows one to define various simulation relations in terms of an antagonistic two-player game. The second component is a software tool that, given two labeled transition systems and simulation definition, is able to check whether this simulation is satisfied between these labeled transition systems.     

Systematic testing and formal verification to validate reactive programs

The use of systematic testing and formal verification in the validation of reactive systems implemented in synchronous languages is illustrated. Systematic testing and formal verification are two techniques for checking the consistency between a program and its specification. The approach to validation is through specification: two system views are developed in addition to the program, a behavioural specification for systematic testing and a logical specification for formal verification. Pursuing both activities, reactive programs can be validated both more efficiently (in terms of costs) and more effectively (in terms of confidence in correctness). This principle is demonstrated here using the well known lift example.