A survey on formal specification and verification of separation kernels

Abstract Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the back- ground including the concept of separation kernel and the comparisons among different kernels. Then, we survey the state of the art on this topic since 2000. Finally, we summa- rize research work by detailed comparison and discussion.

Towards a Methodology for Formal Design and Analysis of Agent Interaction Protocols ——An Investigation in Electronic Commerce

Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led it to be introduced into the development of approaches and tools to check the correctness of electronic commerce protocols. This paper focuses on the research of a method that connects an extension of AUML to model checker SPIN/Promela for the specification and verification of agent interaction protocols (AIP) in electronic commerce. The method presented here allows us to combine the benefits of visual specification with the power of some static analysis and model checking. Some algorithms and rules are developed to permit all visual modeling constructs translated mechanically into some Promela models of AIP, as supported by the model checker SPIN. Moreover, a process is illustrated to guide the specification and verification of AIP. The method is demonstrated thoroughly using the e commerce protocol NetBill as an example.

DEPICT:A High-level Formal Language for Modeling Constraint Satisfaction Problems

The past decade witnessed rapid development of constraint satisfaction technologies, where algorithms are now able to cope with larger and harder problems. However, owing to the fact that constraints are inherently declarative, attention is quickly turning toward developing high-level programming languages within which such problems can be modeled and also solved. Along these lines, this paper presents DEPICT, the language. Its use is illustrated through modeling a number of benchmark examples. The paper continues with a description of a prototype system within which such models may be interpreted. The paper concludes with a description of a sample run of this interpreter showing how a problem modeled as such is typically solved.

THE Z SPECIFICATION DEPENDENCE GRAPH

The lack of existing solutions makes it really hard to understand formal specification languages since the application domain for representations is useful for the purpose of carrying out certain software engineering operations such as slicing and the computation of program metrics.A Z specification dependence graph is presented in this letter. It draws on the strengths of a range of earlier works and adapts them, if necessary, to the Z language.

Data Mapping Principles and Algorithm for Self-Configurable Systems

With the challenges brought by the expansion of network scale,as well as the diversity of the equipments and the complexity of network protocols,many self-configurable systems have been proposed combining formal specification and model finding techniques.In this paper,we pay more attention to formal specifications of network information,i.e.,exploring principles and algorithm to map network information(topology,devices and status,etc.) to Alloy specifications.We first model network information in relational form,which is easy to realize because of the structured feature of network information in nature.Then we map the relational data to Alloy specifications according to our novel data mapping principles and algorithm.Based on the transition of relational data,it is possible to automatically map network information to Alloy specifications.We evaluate our data mapping principles and algorithm by applying them to a practical application scenario.The results illustrate that we can find a model for the task within a tolerant time interval,which implies that our novel approach can convert relational data to Alloy specifications correctly and efficiently.

SDL-TRAN-An Interactive Generator for Formal Description Language SDL

SDL (Specification and Description Language) is an international standardformal description language which has been widely used for the specificationand description of communication systems. SDL is based on the concept ofthe state oriellted description technique - FSM (Finite State Machine). Thispaper reports an interactive generator for SDL, named SDL-TRAN, which canautomatically translate FSM expression into SDL description. Except for itsaatomatic translation part, SDLTRAN includes an userfriendly graPhical ed-itor which is used to get the other part of SDL description which cannot beautomatically translated.

A Formal Software Development Approach Using Refinement Calculus

The advantage of COOZ (Complete Object-Oriented Z) is to specify large scale software, but it does not support refinement calculus. Thus its application is confined for software development. Including refinement calculus into COOZ overcomes its disadvantage during design and implementation. The separation between the design and implementation for structure and notation is removed as well. Then the software can be developed smoothly in the same frame. The combina- tion of COOZ and refinement calculus call build object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In this paper, the development model is established, which is based on COOZ and refinement calculus. Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. As to the implemelltation technology of refinement calculus, the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.

Program Constructionby Verifying Specification

A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition.

Research on formalization of efficient query application problems with compound condition in software development

This paper provides a formalized definition of the application problem of compound condition query （CCQ） and a formal method of applying requirements elicitation based on trace information space derived from trace algebra. With the formalized process of solving the application problem of CCQ, formal requirements specification of application of CCQ is given, a formalized and automatic mapping of the results of requirements elicitation to the formal requirements specification is performed, the software system model and the application code are developed. Through a sample application of comprehensive query on housing information, the feasibility of formalized and automatic software development for the application problem of CCQ is proved. The result has important implications for the other problems regarding formalization and automatic software development.

Function Definition Language FDL andIts Implementation

A Function Definition Language (FDL) is presented. Though de-signed for describing specifications, FDL is also a general-purpose functional pro-gramming language. It uses context-free language as data type, supports patternmatching definition of functions, offers several function definition forms, and is exe-cutable. It is shown that FDL has strong expressiveness, is easy to use and describesalgorithms concisely and naturally. An interpreter of FDL is introduced. Experi-ments and discussion are included.

Pre-post notation is questionable in effectively specifying operations of object-oriented systems

There is a growing tendency for people in the community of object-oriented methods to use preand post-conditions to write formal specifications for opera- tions （methods） of classes. The motivation for trying to take advantage of well established formalism in precisely defining the functionality of operations is laudable, but unfortunately this exercise may be flawed because the use of pre- and post-conditions containing method calls （or similar） with side effects are likely to cause confusion in the interpretation of specifications. This paper analyzes, with comprehensible examples, why using pre-post notation is not effective to specify operations in objectoriented systems in general, discusses existing approaches to using pre-post notation for object-oriented systems, and offers some solutions to the problem.