HOOD方法与形式化技术的集成研究

ＨＯＯＤ是由欧洲ＥＳＡ公司开发的一种面向对象软件结构设计方法,它使用图形,结构化英语和Ａｄａ伪码来描述系统的设计规约,本文首先概述了ＨＯＯＤ方法的基本概念和对它进行的改进,然后提出了一种集成ＨＯＯＤ和形式化技术的方法,借助该方法可以获得更为严格的软件设计规约,最后简要介绍了其机器支持系统。     

开发环境OOPascal的设计和实现

ＮＤＯＯＰ是Ｐａｓｃａｌ面向对象扩充语言，我们进一步为ＮＤＯＯＰ设计和实现了支撑环境ＯＯＰａｓｃａｌ系统，该系统由编辑器、浏览器、转换器、编译器组成。该文阐述了ＯＯＰａｓｃａｌ设计和实现的主要思想，并对该系统的功能、特点、实现技术等作了简要介绍。     

形式描述语言COOZ的集成支撑环境COOZ—Tools

介绍支持面向对象的形式描述语言ＣＯＯＺ的集成支撑环境ＣＯＯＺ－Ｔｏｏｌｓ的设计原则、系统结构、功能、特点和关键的实现技术。ＣＯＯＺ是Ｚ语言的面向对象扩充,从而将形式化语言和面向对象机制有机结合起来。ＣＯＯＺ－Ｔｏｏｌｓ支持基于ＣＯＯＺ的软件开发,它主要由如下工具组成：规格说明编辑、浏览工具、语法语义检查工具、联机帮助工具、项目管理工具。     

一个Pascal的面向对象扩充的设计与实现

本文阐述了ＮＤＯＯＰ的设计和实现的主要思想．ＮＤＯＯＰ是一个Ｐａｓｃａｌ的面向对象扩充，是Ｐａｓｃａｌ的超集，既充分支持面向对象程序设计，又保持了Ｐａｓｃａｌ的原有风格．     

信息系统的LOODS抽象模型

ＬＯＯＤＳ抽象模型是我们提出的一种直接建立在需求分析之上的面向分布式并发／并行信息系统，支持网络计算，面向对象方法与可视化方式的开发方法与工具。它的主导思想是分析，设计的模型化，支撑环境与工具的可视化，面向对象化。     

面向对象软件自动化系统JDAUTO＼0

本文介绍了面向对象经系统ＪＤＡＵＴＯ／０的设计与实现，ＪＯＯＳＬ是一种面向对象软件形式规约语言，基于它，实现了概要设计到详细的自动工具ＰＤＡＵＴＯ和详细设计到Ｃ＋＋代码的自动转换工具ＤＤＡＵＴＯ．     

一种图形化对象式需求定义语言的设计

本文简要讨论了软件需求定义及其语言的有关基本概念，重点介绍了图形化对象式需求定义语言ＮＤＯＲＬ的设计思想以及主要的语言结构与成分．该语言是一种以面向对象方法支持软件需求定义的半形式化语言，具有形象易读、表达力强和便于实现到形式功能规约的转换等特点，并提供了方便的机器支撑.     

信息系统需求分析的面向对象层次分析方法及应用

文章将面向对象分析（ＯＯＡ）,结构化分析（ＳＡ）和数据结构分析（ＤＳＡ）方法相结合,提出了一种信息系统需求分析的面向对象层次分析方法（ＯＯＨＡ）,给出了对象的属性和方法定义以及需求分析的形式化表示方法。使用ＯＯＨＡ方法进行需求分析,层次清晰,对象关系明确,容易实现问题空间到解空间的映射。     

多媒体著作工具的核心与开发技术

Ｔｏｏｌｂｏｏｋ是一种多媒体软件开发工具，采用面向对象的技术为多媒体软件的制作提供了有力的工具。本文介绍在Ｗｉｎｄｏｗｓ环境下Ｔｏｏｌｂｏｏｋ的层次结构，Ｏｐｅｎｓｃｒｉｐｔ语言与性能，讨论Ｔｏｏｌｂｏｏｋ与ＤＬＬ的数据接口技术以及对Ｔｏｏｌｂｏｏｋ开发的一般方法。     

五个著名的面向对象开发方法的评估

近年来，从各个不同的背景提出了很多面向对象的分析和设计方法。比如，ＨＯＯＤ方法，Ｂｕｈｒ方法，Ｂｏｏｃｈ方法，Ｒｕｍｂａｕｇｈ方法和Ｗｉｒｆｓ－Ｂｒｏｃｋ方法。对每个方法按一组准则进行打分面对它们作出评估。评价的准则基于概念、模型、过程和实用性。其目的在于使实践者选择方法时有所依据。     

Formal models for user interface design artefacts

There are many different ways of building software applications and of tackling the problems of understanding the system to be built, designing that system and finally implementing the design. One approach is to use formal methods, which we can generalise as meaning we follow a process which uses some formal language to specify the behaviour of the intended system, techniques such as theorem proving or model-checking to ensure the specification is valid (i.e., meets the requirements and has been shown, perhaps by proof or other means of inspection, to have the properties the client requires of it) and a refinement process to transform the specification into an implementation. Conversely, the approach we take may be less structured and rely on informal techniques. The design stage may involve jotting down ideas on paper, brainstorming with users etc. We may use prototyping to transform these ideas into working software and get users to test the implementation to find problems. Formal methods have been shown to be beneficial in describing the functionality of systems, what we may call application logic, and underlying system behaviour. Informal techniques, however, have also been shown to be useful in the design of the user interface to systems. Given that both styles of development are beneficial to different parts of the system we would like to be able to use both approaches in one integrated software development process. Their differences, however, make this a challenging objective. In this paper we describe models and techniques which allow us to incorporate informal design artefacts into a formal software development process.     

Using formal methods with SysML in aerospace design and engineering

Maintaining design consistency is a critical issue for macro-level aerospace development. The inability to maintain design consistency is a major contributor to cost and schedule overruns. By embedding The Systems Modeling Language (SysML) within a formal logic, formal methods can be used to maintain consistency as a design evolves. SysML, provided with a formal semantics, enables engineers to employ reasoning in the course of a typical model-based development process. Engineers can make use of formal methods within the context of current engineering practice and tools without needing to have special formal methods training. As component subsystems are introduced to refine a design, their assumptions are checked against current assumptions. If new assumptions do not introduce inconsistency, they are added to the model assumptions. If the assumptions render the design inconsistent, they are detected which minimizes potential rework. SysML has a demonstrated capability for top-to-bottom design refinement for large-scale aerospace systems. SysML does not have a formal logic-based semantics. The logical formalism within which SysML is embedded matches the informal semantic of SysML closely. The approach to integrating formal methods with SysML is illustrated with a typical macro-level aerospace design task. The design process produces a design solution which provably satisfies the top level requirements. The example provides evidence that coupling formal methods with SysML can realistically be applied to solve aerospace development problems. The approach results from a number of detailed design trades employing a model-based system development process which used SysML as the model integration framework.     

Review: An information management system for informal design data

Engineering information management may be divided into formal information management, which involves data modelling, data exchange and transaction handling, and informal information management, which is concerned with the organisation and delivery of design advice and design parameter data. This paper describes a system, called Review, which has been developed for the management of informal design information from multiple sources. The system uses a hybrid hypertext/database approach to provide for the indexing and viewing of information sources using arbitrary attribute sets, and for the establishment of relationships between information entities using both static and dynamic links in a hypertext framework. Information may be accessed both by query and by browsing along relationships in the hypertext network. The paper presents an overview of the system design, and examples of its application to design advisory systems and documentation.     

Case-based reasoning techniques to support reusability in a requirement engineering and system design tool

CASA (computer aided systems architecting) is a methodology and tool to support the design of complex technical systems. It combines approaches from systems and requirement engineering and AI. System design in CASA is requirement-driven, and works by a hierarchical stepwise top-down refinement of designs and a hierarchical decision-making process. One important task in CASA deals with the reusability of existing design artifacts and is supported by case-based reasoning techniques. Based on given structural specifications and formal requirements, a search procedure finds the best inexact match in a design base and computes an estimated degree of fulfillment for requirements. The approach employs efficient graph-matching and indexing schemes for case retrieval and structural similarities, and has adapted usual similarity measures to compute degree of fulfillment of requirements. It has been shown by different sample projects that the developed methods can be of great practical assistance to a designer.     

面向对象的建模语言面面观

面向对象的编程技术及其语言的发展,引起了软件工程方法 的变革,简述了面向对象方法与传统方法的不同,介绍当前几种流行的面向对象的建模方法 ,分析了建模辅助工具应具有的基本功能,最后推荐两种性能较好的建模辅助工具。     

ASM-based formal design of an adaptivity component for a Cloud system

The request of formal methods for the specification and analysis of distributed systems is nowadays increasing, especially when considering the development of Cloud systems and Web applications. This is due to the fact that modeling languages currently used in these areas have informal definitions and ambiguous semantics, and therefore their use may be unreliable. Thanks to their mathematical foundation, formal methods can guarantee rigorous system design, leading to precise models where requirements can be validated and properties can be assured, already at the early stages of the system development. In this paper, we present a rigorous engineering process for distributed systems, based on the Abstract State Machines (ASM) formal method. We rely on the foundational notions of ASM ground model and model refinement to obtain a precise model for a client-server application for Cloud systems. This application has been proposed to tackle the problem of making Cloud services usable to different end-devices by adapting on-the-fly the content coming from the Cloud to the different devices contexts. The ASM-based modeling process is supported by a number of validation and verification activities that have been exploited on the component under development to guarantee consistency, correctness, and reliability properties.     

Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System

Reliability of medical devices such as the CARA Infusion Pump Control System is of extreme importance given that these devices are being used on patients in critical condition. The Infusion Pump Control System includes embedded processors and accompanying embedded software for monitoring as well as controlling sensors and actuators that allow the embedded systems to interact with their environments. This nature of the Infusion Pump Control System adds to the complexity of assuring the reliability of the total system. The traditional methods of developing embedded systems are inadequate for such safety-critical devices. In this paper, we study the application of formal methods to the requirements capture and analysis of the Infusion Pump Control System. Our approach consists of two phases. The first phase is to convert the informal design requirements into a set of reference specifications using a formal system, in this case EFSMs (Extended Finite State Machines). The second phase is to translate the reference specifications to the tools supporting formal analysis, such as SCR and Hermes. This allows us to conclude properties of the reference specifications. Our research goal is to develop a framework and methodology for the integrated use of formal methods in the development of embedded medical systems that require high assurance and confidence .