On method statics and dynamics

We view a method as having a static and a dynamic part. The former is concerned with the structure of methods whereas the latter relates to the way in which this structure can be used to build products. Starting with the generic view of a method, the instantiation technique has been used to define a decision-oriented metamodel which, in turn, can be instantiated to yield a representation of a method. These three layers form a comprehensive three-layered architecture for a method representation system. Each layer is composed of its statics and dynamics. The resulting method notation has been used as a basis for building a CASE tool, called Guide, and a CAME tool, called MERU.     

Meta-CASE: Is the game worth the candle?

The current generation of CASE (Computer Aided Software Engineering) tools is too inflexible to provide adequate modelling support. One of the proposed solutions to this problem is the development of so-called CASE shells. A CASE shell is a method independent CASE tool, which may be instantiated with a specific method to become a CASE tool supporting that method. As such, a CASE shell provides complete flexibility. This paper does not address the benefits of CASE shells, as they are completely clear, but focuses on the feasibility of this concept from a theoretical as well as a practical point of view.     

A component framework for system modeling based on high-level replacement systems

The aim of this paper is to present a generic component framework for system modeling that satisfies main requirements for component-based development in software engineering. In this sense, we have defined a framework that can be used, by providing an adequate instantiation, in connection with a large class of semi-formal and formal modeling techniques. Moreover, the framework is also flexible with respect to the connection of components, providing a compositional semantics of components. This means more precisely that the semantics of a system can be inferred from the semantics of its components. In contrast to other component concepts for data type specification techniques, our component framework is based on a generic notion of transformations. In particular, refinements and transformations are used to express intradependencies, between the export interface and the body of a component, and interdependencies, between the import and the export interfaces of different components. The generic component framework generalizes module concepts for different kinds of Petri nets and graph transformation systems proposed in the literature, and seems to be also suitable for visual modeling techniques, including parts of the UML, if these techniques provide a suitable refinement or transformation concept. In this paper the generic approach is instantiated in two steps. First to high-level replacement systems generalizing the transformation concept of graph transformations. In a second step it is further instantiated to low-level and high-level Petri nets. To show applicability we present sample components from a case study in the domain of production automation as proposed in a priority program of the German Research Council (DFG).     

Towards a formalism to produce a programmer assistant CASE tool

A weak specification method important to the area of computer-aided software engineering (CASE) is introduced. The specification language introduced does not require the specification of control flow information. When given a specification consisting of a formula characterizing input constraints of a function and a formula characterizing output constraints, it is possible to synthesize program functions. The synthesis algorithm is guaranteed to find all functions which satisfy the specification. It is shown that when the algorithm is applied to the specifications, it is capable of producing all program structures, including sequences, selections, and iterations. Therefore, the methodology provides for a formal foundation upon which a CASE programmer assistant tool can be built     

A method to build information systems engineering process metamodels

Several process metamodels exist. Each of them presents a different viewpoint of the same information systems engineering process. However, there are no existing correspondences between them. We propose a method to build unified, fitted and multi-viewpoint process metamodels for information systems engineering. Our method is based on a process domain metamodel that contains the main concepts of information systems engineering process field. This process domain metamodel helps selecting the needed metamodel concepts for a particular situational context. Our method is also based on patterns to refine the process metamodel. The process metamodel can then be instantiated according to the organisation’s needs. The resulting method is represented as a pattern system.     

Dynamic verification of C++ generic algorithms

Dynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification one also needs to generate multiple program execution paths and use assertions (to handle while loops, for example), but the authors show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. They include an example of the formal verification of an STL generic algorithm     

An empirical study of the validation process within requirements determination

Abstract. An empirical investigation into the validation process within requirements determination is described in which systems analysts were asked to complete a questionnaire concerning important validation issues. We describe the major validation activities, a set of major problems experienced by the respondents, factors affecting the process and hypotheses for problem explanations. The levels of experience of the respondents and the organizations for which they work appear to be significant.
Analysts employ a very traditional approach, expressing the specification mainly in English, and they experience problems in using over-formal notations in informal situations with users, as well as problems in deriving full benefit from notations when building the specification and detecting its properties. Not all of the specification is validated and tool use is not widespread and does not appear to be effective.
We define the concepts of formal and informal view, and suggest that method and tool use will not necessarily increase in organizations as it is apparent that research into the more effective application of formal notations is necessary. In addition, it is clear that the factors that affect the validation process are not only technical, but individual and organizational, necessitating the development of suitable informal activities which take these factors into account.     

Formalising high-performance systems methodologies

This paper presents a Z formal framework to describe software design methodologies (SDM) for high-performance systems (HPS). The framework consists of two main parts: the characterisation of the main activities in the development of HPS, and the components of the SDM (concepts, artifacts, representation and actions) which are essential for any methodology. The framework relates these two parts by identifying generic components of each activity that can be used to classify and formalise SDM for HPS. This is illustrated in the paper by presenting part of the specification of a well-known method.     

形式化方法在电信服务系统中的应用与研究

为提高电信服务系统的稳定性．把形式化方法引入到电信服务系统的研究中,并用典型的形式化规格语言Z开发电信系统中基本功能的形式化规格,该套形式化规格对拔打电话、建立连接、释放连接、修改密码等操作的进行详细、精确的描述。基于Z语言的形式化规格可以应用于电信服务系统开发过程的各个阶段．以期减少电信服务系统内部错误的产生、提高稳定性。     

基于Object—Z的UML对象模型的形式化

1 引言 UML作为面向对象的可视化建模语言,己被对象管理集团(OMG)作为面向对象分析和设计的标准,获得了众多工具的支持。UML提供了不同抽象层次的描述以支持面向对象的分析、设计和实施,它从不同的视图描述软件系统,减少了建模的复杂度,更为重要的是建立了基于元模型的体系结构,提供了较为灵活的扩充机制,使开发人员可以根据不同的领域需求定制UML,也易于加入新的建模概念。     

Formal analysis of the Shlaer-Mellor method: Towards a toolkit of formal and informal requirements specification techniques

In this paper, we define a number of tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible use is. We argue that this definition can best be achieved by a formal specification of the tool. This means that for each semi-formal requirements engineering tool we should provide a formal specification that precisely specifies its meaning. We argue that this mutually enhances the formal and semi-formal technique: it makes formal techniques more usable and, as we will argue, at the same time simplifies the diagram-based notations.At the same time, we believe that the tools of the requirements engineer should, where possible, resemble the familiar semi-formal specification techniques used in practice today. In order to achieve this, we should search existing requirements specification techniques to look for a common kernel of familiar semi-formal techniques and try to provide a formalisation for these.In this paper we illustrate this approach by a formal analysis of the Shlaer-Mellor method for object-oriented requirements specification. The formal specification language used in this analysis is LCM, a language based on dynamic logic, but similar results would have been achieved by means of another language. We analyse the techniques used in the information model, state model, process model and communication model of the Shlaer-Mellor method, identify ambiguities and redundancies, indicate how these can be eliminated and propose a formalisation of the result. We conclude with a listing of the tools extracted from the Shlaer-Mellor method that we can add to a toolkit that in addition contains LCM as formal specification technique.     

Formal verification of a generic framework to synthesize SAT-provers

We present in this paper an application of the ACL2 system to generate and reason about propositional satisfiability provers. For that purpose, we develop a framework in which we define a generic S AT-prover based on transformation rules, and we formalize this generic framework in the ACL2 logic, carrying out a formal proof of its termination, soundness, and completeness. This generic framework can be instantiated to obtain a number of verified and executable SAT-provers in ACL2, and this instantiation can be done in an automated way. Three instantiations of the generic framework are considered: semantic tableaux, sequent calculus, and Davis-Putnam-Logeman-Loveland methods.     

基于本体的多域访问控制策略集成研究

本体是共享概念模型的形式化规范说明,是一种能在语义和知识层次上描述信息系统概念模型的建模工具,为解决多域环境中的安全互操作提供了一种新的方法.使用本体及其描述语言,对基于角色的访问控制策略进行了描述,形成一个概念和属性的公理集合（TBox）,并采用ALCN（含有个数限制和补算子的描述逻辑语言）对TBox进行形式化的描述.利用域间角色映射方法来解决多域访问控制策略的集成.使用基于规则的推理技术,定义多域访问控制中的一系列推理规则,实现访问控制领域的推理.基于前述方法实现了OntoAC系统,实验结果表明该方法是有效的.     

On generic method models

The generic method model assumes that methods abound and method engineering and application engineering is done in diverse areas. Therefore, it is necessary to understand the notion of a method independent of information systems and software engineering. The generic model presented here abstracts out from product and process meta-models to define a system of concepts that can be used in any domain. Additionally, it integrates in it essential features of methods like quality checking, guidance, backtracking, and traceability. The proposed generic model looks upon a method in two parts, the static and the dynamic parts. The former provides the basic structure of a method whereas the latter is the enactment support provided for application development. The static part provides the notion of method blocks and dependencies between them. Method blocks can be enacted. The generic model is a triple <M, D, E> where M is the set of method blocks, D is the set of dependencies between method blocks, and E is the enactment mechanism.     

A metamodeling approach for pattern specification and management

The formal specification of design patterns is central to pattern research and is the foundation of solving various pattern-related problems.In this paper,we propose a metamodeling approach for pattern specification,in which a pattern is modeled as a meta-level class and its participants are meta-level references.Instead of defining a new metamodel,we reuse the Unified Modeling Language(UML)metamodel and incorporate the concepts of Variable and Set into our approach,which are unavailable in the UML but essential for pattern specification.Our approach provides straightforward solutions for pattern-related problems,such as pattern instantiation,evolution,and implementation.By integrating the solutions into a single framework,we can construct a pattern management system,in which patterns can be instantiated,evolved,and implemented in a correct and manageable way.     

Database reverse engineering: From requirements to CARE tools

This paper analyzes the requirements that CASE tools should meet for effective database reverse engineering (DBRE), and proposes a general architecture for data-centered applications reverse engineering CASE environments. First, the paper describes a generic DBMS-independent DBRE methodology, then it analyzes the main characteristics of DBRE activities in order to collect a set of desirable requirements. Finally, it describes DB-MAIN, an operational CASE tool developed according to these requirements. The main features of this tool that are described in this paper are its unique generic specification model, its repository, its transformation toolkit, its user interface, the text processors, the assistants, the methodological control and its functional extensibility. Finally, the paper describes five real-world projects in which the methodology and the CASE tool were applied.     

Semantics of model views for information exchanges using the industry foundation class schema

The industry foundation classes (IFC) data schema is generic, designed to support the full range of model exchanges needed in the construction industry. For any particular working exchange for some sub-domain of building construction, a set of model view definitions (MVD) is required to specify exactly what information should be exchanged, and in what form and structure the IFC entities are to be used. Defining model view definitions requires principle decisions and workarounds because the IFC itself does not address a number of semantic issues comprehensively. Some of the issues identified and discussed include the typing of objects, instances, geometry, relationships, and rules, which are supported in the IFC schema, and the complexities of exchanging such information accurately between applications. This paper advances the idea of MVD Concepts as an object-oriented and modular mechanism for embedding semantic meaning in model views. We conclude that although the IFC product model schema is richly expressive, it lacks formal definition of its entities, attributes, and relationships. To achieve standardized and re-usable model views, further research towards a modular and logical framework based on formal specification of IFC concepts is recommended. This research is expected to impact the overall interoperability of applications in the building information modeling realm.     

Integration of FMS performance evaluation models using patterns for an information system design

The objective of our work is to create an information system able to integrate different view points concerning the design and the control of a Flexible Manufacturing System. Numerous methods based on generic reference frameworks have been proposed for the modeling of all the aspects of production systems. These models have to be instantiated in order to be applied to specific systems. The difficulties are then to integrate pre-existing models of the studied systems with those obtained by the instantiation of the generic reference framework.

The proposed approach tackles the problem from the information system point of view. A meta-modeling bottom-up approach is presented based on the notion of patterns in order to facilitate the integration step.

An example concerned with the performance evaluation and scheduling of a production system is presented to show how the product viewpoint can be built in order to be integrated later with other viewpoints.     

测试集自动生成工具TUGEN的设计与实现

测试集自动生成工具的研究是协议一致性测试领域中比较活跃的一个分支，本文在对目前已有的各种测试集生成方法进行分析的基础上，提出了一种新的测试集自动生成方法并对它的实现ＴＵＧＥＮ作了介绍．ＴＵＧＥＮ基于一种称为ＥＢＥ的形式模型，ＥＢＥ模型只对协议的外部行为进行描述，而且可以从协议的Ｅｓｔｅｌｌｅ或ＬＯＴＯＳ描述中转化得到．ＴＵＧＥＮ以协议的ＥＢＥ－ＮＦ描述作为输入，使用我们新提出的一套测试事例生成策略，最后产生出ＴＴＣＮ．ＭＰ格式的测试集．我们用Ｘ．２５ＬＡＰＢ协议的ＥＢＥ－ＮＦ描述作为例子，对ＴＵＧＥＮ     

An object-oriented model for the specification of manufacturing systems

The design of advanced manufacturing systems entails a high flexibility in the system specification method, to allow for flexibility and efficiency in coping with the frequent design modifications. Object-oriented specification methods possess the necessary expressiveness and extensibility to allow for such flexibility. In order to obtain a declarative representation of the knowledge of objects, the semantic data model of the frame-based representation method is incorporated. This extended object-oriented model can be used for specifying system behaviors. Within this model, generic object types representing general concepts in manufacturing systems are identified. These generic object types can facilitate the specification of manufacturing systems by means of an object-oriented approach. The application of the model for system specification is illustrated with reference to a typical robotic FMC.