Specifying communication in distributed information systems

We present two logics that allow specifying distributed information systems, emphasizing communication among sites. The low-level logic offers features that are easy to implement but awkward to use for specification, while the high-level logic offers convenient specification features that are not easy to implement. We show that specifications may be automatically translated to in a sound and complete way. In order to prove soundness and completeness, we define our translation as a simple map of institutions. Our result may be useful for making implementation platforms like Corba easier accessible by providing high-level planning and specification methods for communication. Received: 28 September 1998 / 18 November 1999     

Specifying concurrent systems with TSL

The Task Sequencing Language (TSL), which lets programmers specify constraints on the behavior of concurrent programs, is described. The constraints, specified by high-level annotations to Ada programs, are monitored at runtime; when a violation is detected, control is returned to the user, along with information about the nature of the violation. It is argued that such a tool is a necessary crutch for human reasoning capabilities when dealing with the complexities of concurrent process interaction. The first large-scale application of TSL, the specification and validation of a distributed tasking supervisor for Ada, is described     

Specifying safety-critical systems with a decidable duration logic

Punctual timing constraints are important in formal modelling of safety-critical real-time systems. But they are very expensive to express in dense time. In most cases, punctuality and dense-time lead to undecidability. Efforts have been successful to obtain decidability; but the results are either non-primitive recursive or nonelementary. In this paper we propose a duration logic which can express quantitative temporal constraints and punctuality timing constraints over continuous intervals and has a reasonable complexity. Our logic allows most specifications that are interesting in practice, and retains punctuality. It can capture the semantics of both events and states, and incorporates the notions duration and accumulation. We call this logic ESDL (the acronym stands for Event- and State-based Duration Logic). We show that the satisfiability problem is decidable, and the complexity of the satisfiability problem is NEXPTIME. ESDL is one of a few decidable interval temporal logics with metric operators. Through some case studies, we also show that ESDL can specify many safety-critical real-time system properties which were previously specified by undecidable interval logics or their decidable reductions based on some abstractions.     

A transaction-based approach to vertical partitioning forrelational database systems

An approach to vertical partitioning in relational databases in which the attributes of a relation are partitioned according to a set of transactions is proposed. The objective of vertical partitioning is to minimize the number of disk accesses in the system. Since transactions have more semantic meanings than attributes, this approach allows the optimization of the partitioning based on a selected set of important transactions. An optimal binary partitioning (OBP) algorithm based on the branch and bound method is presented, with the worst case complexity of O(2ⁿ), where n is the number of transactions. To handle systems with a large number of transactions, an algorithm BPi with complexity varying from O(n) to O(2ⁿ) is also developed. The experimental results reveal that the performance of vertical partitioning is sensitive to the skewness of transaction accesses. Further, BPi converges rather rapidly to OBP. Both OBP and BPi yield results comparable with that of global optimum obtained from an exhaustive search     

Specifying real-time properties in autonomic systems

Increasingly, computer software must adapt dynamically to changing conditions. The correctness of adaptation cannot be rigorously addressed without precisely specifying the requirements for adaptation. In many situations, these requirements involve absolute time, in addition to a logical ordering of events. This paper introduces an approach to formally specifying such timing requirements for adaptive software. We introduce TA-LTL, a timed adaptation-based extension to linear temporal logic, and use this logic to specify three timing properties associated with the adaptation process: safety, liveness, and stability. A dynamic adaptation scenario involving interactive audio streaming software is used to illustrate the timed temporal logic. A number of related papers and technical reports of the Software Engineering and Network Systems Laboratory can be found at the following URL: http://www.cse.msu.edu/sens.     

Specifying and verifying requirements of real-time systems

An approach to specification of requirements and verification of design for real-time systems is presented. A system is defined by a conventional mathematical model for a dynamic system where application specific states denote functions of real time. Specifications are formulas in duration calculus, a real-time interval logic, where predicates define durations of states. Requirements define safety and functionality constraints on the system or a component. A top-level design is given by a control law: a predicate that defines an automation controlling the transition between phases of operation. Each phase maintains certain relations among the system states; this is analogous to the control functions known from conventional control theory. The top-level design is decomposed into an architecture for a distributed system with specifications for sensor, actuator, and program components. Programs control the distributed computation through synchronous events. Sensors and actuators relate events with system states. Verification is a deduction showing that a design implies requirements     

Specifying the dynamic behavior of management systems

Decision making in any complex system is a very difficult task. In Man, decisions are reached as a result of trying to satisfy both conscious and unconscious goals. To emulate this in a computer system we need to find a way of representing goals and modeling the decision making process. This paper describes a model for decision making in the context of the management of distributed computer systems, and discusses the implications for the representation of goals and other information used during the decision making process. The work described in this paper was performed in the ESPRIT II project DOMAINS. This project is concerned with developing an architecture for the integrated management of all resources in a networked system. The emphasis of this paper lies in modeling rather than implementation.     

使用SystemC进行基于事务的验证

分析了使用SystemC的基于事务的验证方法。它应用于一个具体项目的开发,并与传统的验证方法作了对比,证明它在验证效率和验证环境设计效率上均有明显优势。     

Specifying distributed multi-agent systems in chemical reaction metaphor

This paper presents an application of Chemical Reaction Metaphor (CRM) in distributed multi-agent systems (MAS). The suitability of using CRM to model multi-agent systems is justified by CRM's capacity in specifying dynamic features of multi-agent systems. A case study in an agent-based e-learning system (course material updating) demonstrates how the CRM based language, Gamma, can be used to specify the architectures of multi-agent systems. The effectiveness of specifying multi-agent systems in CRM from the view point of software engineering is further justified by introducing a transformational method for implementing the specified multi-agent systems. A computation model with a tree-structured architecture is proposed to base the design of the specified multi-agent system during the implementation phase. A module language based on the computation model is introduced as an intermediate language to facilitate the translation of the specification of multi-agent systems. The multicast networking technology pragmatizes the implementation of communications and synchronization among distributed agents. The paper also discusses the feasibility of implementing an automatic translation from the Gamma specification to a program in the module language. This work is supported by University of Houston-Downtown Organized Research Committee.     

Specifying Cash-Point with DisCo

We describe how the cash-point service problem of Formal Methods ’99 is specified using DisCo [Dis, JKS91]. Received January 2000 / Accepted in revised form December 2000     

Expert systems integrated with information systems

Amongst the users of the AIDA applications there is a rapidly growing interest in the use of expert systems, not as independent systems, but as logical extensions of their already existing information systems. In this paper a prototype system (IDEA) will be described that consists of a set of utilities for the construction of an expert system within the context of an AIDA application. Although IDEA does not excel in sophisticated knowledge representations nor in search strategies (the development of which was not our primary concern) it is able to demonstrate that the facilities provided by AIDA together with the IDEA facilities result in an expert system which is characterized by a high degree of integration with the already operational information system.     

一种基于事务的SoC功能验证方法

本文介绍了基于事务的SoC验证方法,详细说明了事务、事务处理器的概念和事务级验证平台的功能结构.Synopsys公司的RVM验证方法学是当前比较流行的基于事务的SoC验证方法,文中详细介绍了RVM验证平台的层次结构.并且以一个UART模块的功能验证为例,描述了如何利用RVM验证方法学搭建一个高效的可重用的验证平台.     

Specifying recursive agents with GDTs

The purpose of this article is to formalise the notion of recursive agent by extending the Goal Decomposition Tree formalism (GDT). A formal semantics of this decomposition is given, as well as the definition of operators to introduce various ways of recursively defining agents. Design patterns, that show various use cases for recursive agents, are also presented. Finally, to preserve the essential GDT characteristics (that is to allow the verification of agents behaviours), we give proof schemas that allow a proof of the correctness of a recursive agent.     

Specifying coalgebras with modal logic

We propose to use modal logic as a logic for coalgebras and discuss it in view of the work done on coalgebras as a semantics of object-oriented programming. Two approaches are taken: First, standard concepts of modal logic are applied to coalgebras. For a certain kind of functor it is shown that the logic exactly captures the notion of bisimulation and a complete calculus is given. Examples of verifications of object properties are given. Second, we discuss the relationship of this approach with the coalgebraic logic of Moss (Coalgebraic logic, Ann Pure Appl. Logic 96 (1999) 277–317.).     

Specifying Graph-like Diagrams with Dia Gne

This extended abstract demonstrates that creating editors and environments for visual languages becomes considerably easier when restricting the class of visual languages. The presented approach considers graph-like languages whose diagrams consist of nodes and edges with different types. The specification method allows to describe such graphs in terms of their node and edge types and makes use of constraints in order to express syntactic properties. The DIA GEN system is used to generate running editors from such specifications.     

Linking soft systems methodology with data-focused information systems development

Abstract. Where the soft systems methodology (SSM) is used in the development of organizational information systems a clear division exists between the use of SSM to identify what information systems are required and conventional development activities in which it is decided how those information systems will be supplied. Discussion of how SSM might be more closely linked to conventional information systems development methodologies has been concentrated upon process-focused approaches to information systems development. This has been partly due to a perceived mismatch between the underlying philosophies of SSM and the alternative data-focused development methodologies. This paper argues that this perception may be mistaken; not only do the existing forms of data analysis have a large though unacknowledged subjective component but the SSM concept of appreciation may provide a model of human sense-making that the data-focused approaches currently lack and from which they may benefit. The idea of appreciation also allows that an alternative, interpretative form of data analysis might be used within SSM. It is therefore the conclusion of this paper that some closer integration of SSM with data-focused approaches to information systems development is theoretically feasible and may be practically desirable. A number of possible advantages of such integration are described.     

基于CORBA封装已有系统实现信息系统集成

针对当前各类信息系统相互之间集成难度大、可伸缩性差的缺点,提出采用ＣＯＲＢＡ技术已有系统进行封装,构造成多个功能代理处理各应用系统之间的互操作,使应用系统更易实现信息集成,并以ＭＲＰⅡ／ＥＲＰ系统与ＣＡＤ／ＣＡＰＰ系统之间实现应用集成的实例作为说明。     

Problems with strategic information systems frameworks

In the mid 1980s a number of frameworks appeared for analysing information systems from a strategic perspective. A dozen generic problems with these strategic information systems frameworks (SIS frameworks) are described, including the following. Most SIS frameworks are American in origin (and hence may be culturally bound). Since there are a large number of frameworks in existence, each is at best a relative version of the truth. Also because of the variety it may be costly to find an appropriate framework, and even more costly to find an inappropriate one. SIS frameworks are mostly post hoc applications of general strategic frameworks and so do not incorporate any special features of the computer world which might not have been apparent when the frameworks were devised. It is argued that SIS frameworks are externally imposed meanings and will stifle creativity by focusing attention away from bright ideas generated internally, will create the conditions for a power struggle for that meaning, and tend to move the locus of control for SISs outside the company. Finally, even the simplest framework may be understood in more than one way, creating the possibility of further hidden divisions.     

Specifying real-time properties with metric temporal logic

This paper is motivated by the need for a formal specification method for real-time systems. In these systemsquantitative temporal properties play a dominant role. We first characterize real-time systems by giving a classification of such quantitative temporal properties. Next, we extend the usual models for temporal logic by including a distance function to measure time and analyze what restrictions should be imposed on such a function. Then we introduce appropriate temporal operators to reason about such models by turning qualitative temporal operators into (quantitative) metric temporal operators and show how the usual quantitative temporal properties of real-time systems can be expressed in this metric temporal logic. After we illustrate the application of metric temporal logic to real-time systems by several examples, we end this paper with some conclusions.Part of this research has been performed at the Eindhoven University of Technology when the author was working in ESPRIT project 937: Debugging and Specification of Ada Real-Time Embedded Systems (DESCARTES).