Specifications: Formal and informal—a case study

Formal specifications (algebraic) are given for an informally specified small subsystem of the Change Management Automatic Build System. A comparison of the two specifications shows that although informal specifications are easier to read, the formal specifications are clearer, specify operation domains precisely, define the interaction between the operations, show the incompleteness of the informal specifications and are devoid of implementation details. The formal specifications pointed to the need of a function not in the subsystem whose inclusion would improve the system design. This inclusion is now being considered. However, the use of algebraic specifications requires practice and experience. Although the formal specification of large systems is somewhat impractical at the moment, experience in using formal specifications can lead to better informal specifications.     

Modifying LOTOS Specifications by Means of Automatable Formula-Based Integrations

The use of good (formal) specifications of software components produces a good characterization of their functionalities. This fact eases the modifiability of a module specification due to a change of requirements or to the need of an enhancement of its functionalities after the delivery to the users, and then, in general, eases also the reusability of a module. Moreover, if existing modules have a specification not based on a natural language but on the well-given syntax of a specification language, it is possible to process the needed modifications in an automatic way. This work presents a method to derive the modifications of the specification of an existing module (given by means of the LOTOS language) from a characterization of the environment, in which the new module has to be used, given by means of temporal logic formulae. The method consists of tableau-based rules that build the due modifications, and always produces a fitting solution for formulae that can be satisfied and belong to a given class.     

An Empirical Study on the Impact of Automation on the Requirements Analysis Process

Requirements analysis is an important phase in a software project. The analysis is often performed in an informal way by specialists who review documents looking for ambiguities, technical inconsistencies and incomplete parts. Automation is still far from being applied in requirements analyses, above all since natural languages are informal and thus difficult to treat automatically. There are only a few tools that can analyse texts. One of them, called QuARS, was developed by the Istituto di Scienza e Tecnologie dell＇Informazione and can analyse texts in terms of ambiguity. This paper describes how QuARS was used in a formal empirical experiment to assess the impact in terms of effectiveness and efficacy of the automation in the requirements review process of a software company.     

Interchanging Specifications and Implementations in Evolutionary Prototyping

The strategy of retrofitting quality onto a prototype and evolving it into a production quality system has at best led to severe problems and at worst to a complete failure. The present work reports on an environment and methodology that supports the development of high quality prototypes that can easily accommodate changes so that the prototypes can be evolved into production quality systems. An outline of the environment incorporating an architectural mechanism and associated tools that accommodates the intertwining of algebraic specifications, known as ADTSPEC, and implementations in a modular programming language, PARADOX PASCAL, is presented. A framework for applying the environment in the context of evolutionary development is detailed. An illustrative application is also presented. It demonstrates the effectiveness of the work, to support user participation at each stage of evolution and the engineering of high quality prototypes constructed in a systematic manner, incorporating the degree of rigour that is appropriate to the clarity of requirements.     

软件库调用规约挖掘

软件库调用规约是一种描述软件库提供函数正确调用顺序的规约.客户代码应按此规约描述的内容调用函数,否则可能引入缺陷,从而降低软件的可信性.由于能够描述可信软件应该满足的性质,软件库调用规约在可信软件、模型检测等研究中扮演特殊的角色.但是,受制于编写规约的巨大代价,软件库通常并不提供已编写好的调用规约.为此,研究者提出了各种自动挖掘此种规约的方法.阐述了其中代表性的方法及其最新的研究进展,并在此基础上探讨了将来的研究方向.     

Formal test specifications in IEEE POSIX

The role of formal methods is examined in the context of the process of developing and adopting open standards. Against the broad backdrop of concerns for improving the quality of standards, issues of conformance assessment, test specification, and test methodology guidelines are considered. The experience gained from the attempts to formalize the test specifications for POSIX 2003.5 is presented as lessons learned. The tradeoffs associated with the various formal methods are considered in terms of the properties of common semantic model for assertions languages. The intent here is to collect the common features in a form that provides insights on issues such as encapsulation and inheritance of specifications, inter-operation semantics, state and control structures for assertions, and name space management conventions.     

Efficient symbolic computation of process expressions

This paper describes three optimization techniques for the eb³ process algebra. The optimizations are expressed in a new deterministic operational semantics which is shown to be trace-equivalent to a traditional non-deterministic operational semantics. Internal action transitions are eliminated by an efficient preruntime analysis of the structure of a process expression. Execution environments are used to optimize variable instantiation using lazy evaluation. Non-determinism is eliminated by returning a choice between possible transitions. This new operational semantics is implemented in the eb³pai process algebra interpreter to support the eb³ method. The goal of this method is to automate the development of information systems using, among other mechanisms, efficient symbolic computation of process expressions.     

On the existence of translations of structured specifications

We provide a set of sufficient conditions for the existence of translations of structured specifications across specification formalisms. The most basic condition is the existence of a translation between the logical systems underlying the specification formalisms, which corresponds to the unstructured situation. Our approach is based upon institution theory and especially upon a recent abstract approach to structured specifications in which both the underlying logics and the structuring systems are treated fully abstractly. Hence our result is applicable to a wide range of actual specification formalisms that may employ different logics as well as different structuring systems, and is very relevant within the context of the fastly developing heterogeneous specification paradigm.     

Pattern Matching and Membership for Hierarchical Message Sequence Charts

Several formalisms and tools for software development use hierarchy in system design, for instance statecharts and diagrams in UML. Message sequence charts (MSCs) are a standardized notation for asynchronously communicating processes. The norm Z.120 also includes hierarchical HMSCs. Algorithms on MSCs rarely take into account all possibilities covered by the norm. In particular, hierarchy is not taken into account since the models that are usually considered are (flat) MSC-graphs, that correspond to the unfolding of hierarchical HMSCs. However, complexity can increase exponentially by unfolding. The aim of this paper is to show that basic algorithms can be designed such that they avoid the costly unfolding of hierarchical MSCs and HMSCs. We show this for the membership and the pattern matching problem. We prove that the membership problem for hierarchical HMSCs is PSPACE-complete. Then we describe a polynomial time algorithm for the pattern matching problem on hierarchical MSCs. The results were obtained while B. Genest was affiliated with LIAFA, Université Paris 7.     

基于形式规格说明的构件匹配

构件匹配依靠精确描述构件的语义,而形式规格说明基于严格的数学概念和理论。将两者结合起来,首先利用Z语言描述属性、方法和构件的类型,并在此基础上,通过一个例子,给出了各种匹配机制的公理描述。最后,介绍了构件匹配的一个重要应用——构件检索。     

A formal model of composing components: the TLA+ approach

In this paper, a method for writing composable TLA⁺ specifications that conform to the formal model called Masaccio is introduced. Specifications are organized in TLA⁺ modules that correspond to Masaccio components by means of a trace-based semantics. Hierarchical TLA⁺ specifications are built from atomic component specifications by parallel and serial composition that can be arbitrary nested. While the rule of parallel composition is a variation of the classical joint-action composition, the authors do not know about a reuse method for the TLA⁺ that systematically employs the presented kind of a serial composition. By combining these two composition rules and assuming only the noninterleaving synchronous mode of an execution, the concurrent, sequential, and timed compositionality is achieved.     

TIDE: A Generic Debugging Framework — Tool Demonstration —

A language specific interactive debugger is one of the tools that we expect in any mature programming environment. We present applications of TIDE: a generic debugging framework that is related to the ASF+SDF Meta-Environment. TIDE can be applied to different levels of debugging that occur in language design.Firstly, TIDE was used to obtain a full-fledged debugger for language specifications based on term rewriting. Secondly, TIDE can be instantiated for any other programming language, including but not limited to domain specific languages that are defined and implemented using ASF+SDF.We demonstrate the common debugging interface, and indicate the amount of effort needed to instantiate new debuggers based on TIDE.     

Program Synthesis from Formal Requirements Specifications Using APTS

Formal specifications of software systems are extremely useful because they can be rigorously analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. To transfer this confidence to the actual source code implementation, a formal link is needed between the specification and the implementation. Generating the implementation directly from the specification provides one such link. A program transformation system such as Paige's APTS can be useful in developing a source code generator. This paper describes a case study in which APTS was used to produce code generators that construct C source code from a requirements specification in the SCR (Software Cost Reduction) tabular notation. In the study, two different code generation strategies were explored. The first strategy uses rewrite rules to transform the parse tree of an SCR specification into a parse tree for the corresponding C code. The second strategy associates a relation with each node of the specification parse tree. Each member of this relation acts as an attribute, holding the C code corresponding to the tree at the associated node; the root of the tree has the entire C program as its member of the relation. This paper describes the two code generators supported by APTS, how each was used to synthesize code for two example SCR requirements specifications, and what was learned about APTS from these implementations.     

Response to “the formal specification of safety requirements for storing explosives”

This short communication is a response to [MuS93] investigating their ACS system specification. The main point in this paper is that executing specifications can be used as a feasible way of validating them. It is essential to have tool support which enables one to write a generally not executable specification, and then prototype (parts of) it directly in the specification language, without translating it into some other prototyping language.     

Component composition preserving behavioral contracts based on communication traces

This paper investigates the compositional properties of reusable software components defined with explicit dependencies and behavioural contracts expressing rely-guarantee specifications in the form of communication traces. In this setting, connection of components through their matching ports is indeed compositional and yields a new component or composite that respects its constituents’ contracts. Thus the behaviour of the composite is computed from the behaviours of its constituents and is known to conform to the contracts without any new proof.     

Incremental mining of information interest for personalized web scanning

Businesses and people often organize their information of interest (IOI) into a hierarchy of folders (or categories). The personalized folder hierarchy provides a natural way for each of the users to manage and utilize his/her IOI (a folder corresponds to an interest type). Since the interest is relatively long-term, continuous web scanning is essential. It should be directed by precise and comprehensible specifications of the interest. A precise specification may direct the scanner to those spaces that deserve scanning, while a specification comprehensible to the user may facilitate manual refinement, and a specification comprehensible to information providers (e.g. Internet search engines) may facilitate the identification of proper seed sites to start scanning. However, expressing such specifications is quite difficult (and even implausible) for the user, since each interest type is often implicitly and collectively defined by the content (i.e. documents) of the corresponding folder, which may even evolve over time. In this paper, we present an incremental text mining technique to efficiently identify the user's current interest by mining the user's information folders. The specification mined for each interest type specifies the context of the interest type in conjunctive normal form, which is comprehensible to general users and information providers. The specification is also shown to be more precise in directing the scanner to those sites that are more likely to provide IOI. The user may thus maintain his/her folders and then constantly get IOI, without paying much attention to the difficult tasks of interest specification and seed identification.     

The Eurotra linguistic specifications: An overview

In this article, we outline the contents of the linguistic specifications of the Eurotra machine translation system. We start in sections 1 and 2 from some of the requirements placed by multilingual MT on the overall design of the linguistic components. We then move on to a characterization of the Eurotra interface structure (section 3), the nature of transfer (section 4), and trends towards more interlingual representations within the project (section 5). Thereafter, we concentrate on the contents of the various levels beside the interface structure (section 6) before giving a brief survey of word structure (section 7) and outlining some areas for further research (section 8).

---

     

高可信IP核交付标准应用

随着数字系统的日益复杂,基于IP(Intellectual Property)的设计方法成为缩短开发周期的必然之选.因此,高可信IP核构建技术成为IP核交付及IP核复用成功的关键.主要研究高可信IP核的构建方法,首先阐述高可信IP核,以及高可信IP核应具有的特点;然后在国内外各大IP核标准的基础上,结合形式化规范技术,给出了一个可操作的高可信IP核文档交付方案.