In this paper, we report on an application of the validation and verification tool kit UPPAAL in the design and analysis of a prototype gear controller, carried out in a joint project between industry and academia. We...
详细信息
ISBN:
(纸本)3540643567
In this paper, we report on an application of the validation and verification tool kit UPPAAL in the design and analysis of a prototype gear controller, carried out in a joint project between industry and academia. We give a detailed description of the formal model of the gear controller and its surrounding environment, and its correctness formalized according to the informal requirements delivered by our industrial partner of the project. the second contribution of this paper is a solution to the problem we met in this case study, namely how to use a tool like UPPAAL, which only provides reachability analysis to verify bounded response time properties. the advantage of our solution is that we need no additional implementation work to extend the existing model-checker, but simple manual syntactical manipulation on the system description.
this paper discusses our experience with literate programming tools in the realm of the modelling and validation of systems. We propose the use of literate programming techniques to structure and control the validatio...
详细信息
A comprehensive object-oriented framework for river water-quality management has been developed. It integrates a range of analytical tools with a graphical user interface and a data management component, and can be li...
详细信息
A comprehensive object-oriented framework for river water-quality management has been developed. It integrates a range of analytical tools with a graphical user interface and a data management component, and can be linked with external applications. It provides an easily extended and user-friendly environment for the assessment and simulation of water quality, the evaluation of alternative pollution-control strategies, and the formulation of optimized control schemes. the framework aims to assist engineers, river authorities, and environment agencies in the analysis and policy-making of river water quality. It has been validated through the studies of the South Nation river system in Canada and the Upper Mersey river system in the United Kingdom.
tools for systemsanalysis often combine different memoryintensive data structures, such as BDDs, tuple sets, and symbolic expressions. When separate packages are used to manipulate these structures, their conflicting...
详细信息
A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. this paper introduces a technique that uses compositionality and dependency analysis to significantly improv...
详细信息
Within the Input/Output Automata framework, we state and prove a general abstraction theorem giving conditions for preservation of safety properties from one automaton to another. We use our abstraction theorem to ver...
详细信息
Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational aut...
详细信息
the proceedings contains 47 papers from the Twelfth IEEE international Automated Software Engineering conference. Topics discussed include: automatic synthesis of recursive programs;graph grammars;distributed cooperat...
详细信息
the proceedings contains 47 papers from the Twelfth IEEE international Automated Software Engineering conference. Topics discussed include: automatic synthesis of recursive programs;graph grammars;distributed cooperative formal method tools;automatic high-quality reengineering of database programs by temporal abstraction;program understanding;application of design patterns;correct-schema-guided synthesis of steadfast programs;software maintenance tools;reverse engineering programs;modular flow analysis for concurrent software;design assistant for distributed embedded systems;and declarative specification of software architectures.
the importance of requirements, which in practice often means natural language requirements, for a successful software project cannot be underestimated. Although requirement analysis has been traditionally reserved to...
详细信息
the importance of requirements, which in practice often means natural language requirements, for a successful software project cannot be underestimated. Although requirement analysis has been traditionally reserved to the experience of professionals, there is no reason not to use various automatic techniques to the same end. In this paper we present Circe, a Web-based environment for aiding in natural language requirements gathering, elicitation, selection, and validation and the tools it integrates. these tools have been used in several experiments both in academic and in industrial environments. Among other features, Circe can extract abstractions from natural language texts, build various models of the system described by the requirements, check the validity of such models, and produce functional metric reports. the environment can be easily extended to enhance its natural language recognition power, or to add new models and views on them.
Most contemporary fourth-generation languages (4GL) are tightly coupled withthe database server, and other subsystems, that are provided by the vendor. As a result, organizations that wish to change database vendors ...
详细信息
Most contemporary fourth-generation languages (4GL) are tightly coupled withthe database server, and other subsystems, that are provided by the vendor. As a result, organizations that wish to change database vendors are typically forced to rewrite their applications using the new vendor's 4GL. the anticipated cost of this redevelopment can deter an organization from changing vendors, hence denying it the benefits that would otherwise result, e.g., the exploitation of more sophisticated database server technology. If tools existed that could reduce the rewriting effort, the large upfront cost of migrating the organization's applications would also be reduced, which could make the transition economically feasible. the ITOC project is part of a large collaborative research initiative between the Centre for Software Maintenance at the University of Queensland and Oracle Corporation. the objective of this project is to design and implement a tool that automatically recovers boththe application structure and the static schema definition of 4GL information system applications. these recovered system components are transformed into constructs that populate Oracle's Designer 2000 CASE repository. An essential component of the ITOC process is to determine the relationships between different columns in the database and between references to those columns and fields that appear within the user interface. this in turn requires analysis of data flow between variables in the 4GL programs. While data flow analysis has been applied in many applications, for example, code optimization and program slicing, this paper presents the results of using data flow analysis in the construction of a novel design recovery tool for 4GL- based information systems. the effectiveness of the approach on legacy commercial applications is described.
暂无评论