Trusted Product Lines

ContextThe paper addresses the use of a Software Product Line approach in the context of developing software for a high-integrity, regulated domain such as civil aerospace. The success of a Software Product Line approach must be judged on whether useful products can be developed more effectively (lower cost, reduced schedule) than with traditional single-system approaches. When developing products for regulated domains, the usefulness of the product is critically dependent on the ability of the development process to provide approval evidence for scrutiny by the regulating authority.ObjectiveThe objective of the work described is to propose a framework for arguing that a product instantiated using a Software Product Line approach can be approved and used within a regulated domain, such that the development cost of that product would be less than if it had been developed in isolation.MethodThe paper identifies and surveys the issues relating the adoption of Software Product Lines as currently understood (including related technologies such as feature modelling, component-based development and model transformation) when applied to high-integrity software development. We develop an argument framework using Goal Structuring Notation to structure the claims made and the evidence required to support the approval of an instantiated product in such domains. Any unsubstantiated claims or missing/sub-standard evidence is identified, and we propose potential approaches or pose research questions to help address this.ResultsThe paper provides an argument framework supporting the use of a Software Product Line approach within a high-integrity regulated domain. It shows how lifecycle evidence can be collected, managed and used to credibly support a regulatory approval process, and provides a detailed example showing how claims regarding model transformation may be supported. Any attempt to use a Software Product Line approach in a regulated domain will need to provide evidence to support their approach in accordance with the argument outlined in the paper.ConclusionProduct Line practices may complicate the generation of convincing evidence for approval of instantiated products, but it is possible to define a credible Trusted Product Line approach.     

The formal definition of a real-time language

Summary This paper presents the formal definition of TOMAL (Task-Oriented Microprocessor Applications Language), a programming language intended for real-time systems running on small processors. The formal definition addresses all aspects of the language. Because some modes of semantic definition seem particularly well-suited to certain aspects of a language, and not as suitable for others, the formal definition employs several complementary modes of definition.The primary definition is axiomatic and is employed to define most statements of the language. Simple, denotational (but not lattice-theoretic) semantics complement the axiomatic semantics to define type-related features, such as binding of names to types, data type coercions, and evaluation of expressions. Together, the axiomatic and denotational semantics define all features of the sequential language. An operational definition is used to define real-time execution, and to extend the axiomatic definition to account for all aspects of concurrent execution. Semantic constraints, sufficient to guarantee conformity of a program with the axiomatic definition, can be checked by analysis of a TOMAL program at compilation.     

Trends in software reuse research: A tertiary study

ContextThe reuse of software has been a research topic for more than 50 years. Throughout that time, many approaches, tools and proposed techniques have reached maturity. However, it is not yet a widespread practice and some issues need to be further investigated. The latest study on software reuse trends dates back to 2005 and we think that it should be updated.ObjectiveTo identify the current trends in software reuse research.MethodA tertiary study based on systematic secondary studies published up to July 2018.ResultsWe identified 4,423 works related to software reuse, from which 3,102 were filtered by selection criteria and quality assessment to produce a final set of 56 relevant studies. We identified 30 current research topics and 127 proposals for future work, grouped into three broad categories: Software Product Lines, Other reuse approaches and General reuse topics.ConclusionsFrequently reported topics include: Requirements and Testing in the category of Lifecycle phases for Software Product Lines, and Systematic reuse for decision making in the category of General Reuse. The most mentioned future work proposals were Requirements, and Evolution and Variability management for Software Product Lines, and Systematic reuse for decision making. The identified trends, based on future work proposals, demonstrate that software reuse is still an interesting area for research. Researchers can use these trends as a guide to lead their future projects.     

Tabular表达式的指称语义研究

Tabular 表达式是一种采用表格化结构组织函数或关系的形式化描述工具,在需求工程领域中具有广泛的应用,为Tabular 表达式建立形式的语义模型是非常必要的.针对Tabular 表达式通用模型,给出了Tabular 表达式的形式文法及指称语义.通过定义形式文法中各语法单元的语义指派方程,描述了Tabular 表达式的指称语义,分别对传统类型Tabular 表达式和新类型Tabular 表达式中一些典型表类型的指称语义进行了描述,并与其他几种Tabular 表达式的语义描述方法进行了比较.分析结果表明：该语义描述方法不仅准确描述了Tabular 表达式的语义,而且不再受Tabular 表达式模型和Tabular 表达式类型的限制,打破了现有方法的局限性,是一种非常有效的方法.     

Event-based operational semantics and a consistency result for real-time concurrent processes with action refinement

In this paper an event-based operational interleaving semantics is proposed for real-time processes,for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics.     

Web Services在软件生产线中的应用

软件生产线与Web服务分别是软件工程与分布式计算领域中两个新兴的热门话题。本文根据软件生产线各阶段的活动阐述如何将Web服务应用于软件生产线,并结合一个实际的 软件生产线系统SoftMaker讨论Web服务的具体应用。     

Generic semantics of feature diagrams

Feature Diagrams (FDs) are a family of popular modelling languages used to address the feature interaction problem, particularly in software product lines, FDs were first introduced by Kang as part of the FODA (Feature-Oriented Domain Analysis) method back in 1990. Afterwards, various extensions of FODA FDs were introduced to compensate for a purported ambiguity and lack of precision and expressiveness. However, they never received a formal semantics, which is the hallmark of precision and unambiguity and a prerequisite for efficient and safe tool automation.The reported work is intended to contribute a more rigorous approach to the definition, understanding, evaluation, selection and implementation of FD languages. First, we provide a survey of FD variants. Then, we give them a formal semantics, thanks to a generic construction that we call Free Feature Diagrams (FFDs). This demonstrates that FDs can be precise and unambiguous. This also defines their expressiveness. Many variants are expressively complete, and thus the endless quest for extensions actually cannot be justified by expressiveness. A finer notion is thus needed to compare these expressively complete languages. Two solutions are well-established: succinctness and embeddability, that express the naturalness of a language. We show that the expressively complete FDs fall into two succinctness classes, of which we of course recommend the most succinct. Among the succinct expressively complete languages, we suggest a new, simple one that is not harmfully redundant: Varied FD (VFD). Finally, we study the execution time that tools will need to solve useful problems in these languages.     

On product logic

In this paper we prove that the class of product algebras is a variety of bounded hoops, that this variety is the equivalent algebraic semantics (in the sense of [1]) of Product logic [11] and that the only axiomatic extension of Product logic that has the Deduction–Detachment Theorem is the Classical propositional logic.     

A fixpoint semantics of Horn sentences based on substitution sets

The formal semantics of a given Horn sentence is usually defined as a set of ground atoms, which is really the minimal Herbrand interpretation of the Horn sentence, by both model-theoretic and fixpoint approaches. In the present paper, we propose another denotational semantics of a Horn sentence, denoting the set of substitutions with which atoms are derivable by unit deduction from the Horn sentence to get a direct correspondence between the semantics of the Horn sentence and the answer set concerned with its computation, and give denotational semantics even when the Horn sentence is unsatisfiable. In accordance with the unit deductions from a Horn sentence, we define a continuous function from a direct product of powersets of a substitution set to itself, and regard the least fixpoint of the function as the semantics, which can provide the answer set for computations of the Horn sentence.     

Towards a semantics-based information theory

We develop a formal framework to give computer programs an abstract interpretation as information transformers. Then the quantitative relation between input and output information is investigated. Our theory is based oninformation domains, a refinement of the classical domains used in denotational semantics, and on the theory of abstract interpretation of functional languages.     

Non-deterministic data types: models and implementations

Summary The model theoretic basis for (abstract) data types is generalized from algebras to multi-algebr as in order to cope with non-deterministic operations. A programming oriented definition and a model theoretic criterion (called simulation) for implementation of data types are given. To justify the criterion w.r.t. the definition, an abstract framework linking denotational semantics of programming languages and model theory of data types is set up. A set of constraints on a programming language semantics are derived which guarantee that simulation implies implementation. It is argued that any language supporting data abstraction does fulfill these constraints. As an example a simple but expressive language L is defined and it is formally proved that L does conform to these restrictions.     

Constructing language processors with algebra combinators

Modular Monadic Semantics (MMS) is a well-known mechanism for structuring modular denotational semantic definitions for programming languages. The principal attraction of MMS is that families of language constructs can be independently specified and later combined in a mix-and-match fashion to create a complete language semantics. This has proved useful for constructing formal, yet executable, semantics when prototyping languages. In this work we demonstrate that MMS has an additional software engineering benefit. In addition to composing semantics for various language constructs, we can use MMS to compose various differing semantics for the same language constructs. This capability allows us to compose and reuse orthogonal language tasks such as type checking and compilation. We describe algebra combinators, the principal vehicle for achieving this reuse, along with a series of applications of the technique for common language processing tasks.     

A Dialogue Game Protocol for Multi-Agent Argument over Proposals for Action

We present the syntax and semantics for a multi-agent dialogue game protocol which permits argument over proposals for action. The protocol, called the Persuasive Argument for Multiple Agents (PARMA) Protocol, embodies an earlier theory by the authors of persuasion over action which enables participants to rationally propose, attack, and defend, an action or course of actions (or inaction). We present an outline of both an axiomatic and a denotational semantics, and discuss implementation of the protocol, in the context of both human and artificial agents.     

Approaching a formal framework for graphics software standards

A graphics software standard has to specify precisely what the software is expected to do. For this purpose, the paper exhibits a formal framework for the specification of software modules which may be structured hierarchically and which may be based on abstract data types. An important aspect concerns the special mathematical semantics of the data types: The semantics of a type is its class of all finitely generated models. This semantics enables a uniform definition of a standard which, nevertheless, may cover a large variety of implementations on very different graphics hardware devices. The kernel of this approach is some axiomatic characterization of the notion of finitely generated images. Another important aspect is that, from such a formal software specification, an implementation may be derived. At least in principle, the careful documentation of such a program derivation could serve as a basis for a verification-oriented certification of graphics standard implementations.     

The semantics of the combination of atomized statements and parallel choice

In this paper we define a uniform language that is an extension of the language underlying the process algebraPA. One of the main extensions of this language overPA is given by so-called atomizing brackets. If we place these brackets around a statement then we treat this statement as an atomic action. Put differently, these brackets remove all interleaving points. We present a transition system for the language and derive its operational semantics. We show that there are several options for defining a transition system such that the resulting operational semantics is a conservative extension of the semantics forPA. We define a semantic domain and a denotational model for the language. Next we define a closure operator on the semantic domain and show how to use this closure operator to derive a fully abstract denotational semantics. Then the algebraic theory of the language is considered. We define a collection of axioms and a term rewrite system based on these axioms. Using this term rewrite system we are able to identify normal forms for the language. It is shown that these axioms capture the denotational equality. It follows that if two terms are provably equal then they have the same operational semantics. Finally, we show how to extend the axiomatization in order to axiomatize its operational equivalence.     

Vivid: A framework for heterogeneous problem solving

We introduce Vivid, a domain-independent framework for mechanized heterogeneous reasoning that combines diagrammatic and symbolic representation and inference. The framework is presented in the form of a family of denotational proof languages (DPLs). We present novel formal structures, called named system states, that are specifically designed for modeling potentially underdetermined diagrams. These structures allow us to deal with incomplete information, a pervasive feature of heterogeneous problem solving. We introduce a notion of attribute interpretations that enables us to interpret first-order relational signatures into named system states, and develop a formal semantic framework based on 3-valued logic. We extend the assumption-base semantics of DPLs to accommodate diagrammatic reasoning by introducing general inference mechanisms for the valid extraction of information from diagrams, and for the incorporation of sentential information into diagrams. A rigorous big-step operational semantics is given, on the basis of which we prove that the framework is sound. We present examples of particular instances of Vivid in order to solve a series of problems, and discuss related work.     

A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++

We introduce a translation of the simply typed λ-calculus into C++, and give a mathematical proof of the correctness of this translation. For this purpose we develop a suitable fragment of C++ together with a denotational semantics. We introduce a formal translation of the λ-calculus into this fragment, and show that this translation is correct with respect to the denotational semantics. We show as well a completeness result, namely that by translating λ-terms we obtain essentially all C++ terms in this fragment. We introduce a mathematical model for the evaluation of programs of this fragment, and show that the evaluation computes the correct result with respect to this semantics.     

A layered semantics for a parallel object-oriented language

We develop a denotational semantics for POOL, a parallel object-oriented programming language. The main contribution of this semantics is an accurate mathematical model of the most important concept in object-oriented programming: the object. This is achieved by structuring the semantics in layers working at three different levels: for statements, objects and programs. For each of these levels we define a specialized mathematical domain of processes, which we use to assign a meaning to each language construct. This is done in the mathematical framework of complete metric spaces. We also define operators that translate between these domains. At the program level we give a precise definition of the observable input/output behaviour of a particular program, which could be used at a later stage to decide the issue of full abstractness. We illustrate our semantic techniques by first applying them to a toy language similar to CSP.This paper describes work done in ESPRIT Basic Research Action 3020,Integration.