3,458 papers · page 157 of 173
This paper presents a mechanizable framework for specifying, developing, and reasoning about complex systems. The framework combines features from algebraic specifications, abstract state machines, and refinement calculus, all couched in a categorical setting. In particular, we s…
Verification and Validation (V&V) of software for critical embedded control systems often consumes upto 70% of the development resources. Testing is one of the most frequently used V&V technique for verifying such systems. Many regulatory agencies that certify control systems for…
Summary form only given, as follows. A concurrent real-time system is a system of many components, that should deliver the result in a particular time interval. The design of such a system is generally complex, with high possibility of errors. Thus it is very important to be able…
Reverse engineering a program constructs a high-level representation suitable for various software development purposes such as documentation or reengineering. Unfortunately however, there are no established guidelines to assess the adequacy of such a representation. We propose t…
The Unified Modeling Language has become widely accepted as a standard in software development. Several tools have been produced to support UML model validation. These tools translate a UML model into a validation language such as PROMELA. However they have some shortcomings: the…
The paper describes the application of an automated verification tool to a software model developed at Ford Motor Company. Ford already has in place an advanced model-based software development framework that employs the Matlab(R), Simulink(R), and Stateflow(R) modeling tools. Du…
The paper presents a novel approach for automated test data generation of imperative programs containing integer, boolean and/or float variables. Our approach is based on consistency techniques integrating integer and float variables. We handle statement, branch and path coverage…
Previous work on domain-specific deductive program synthesis described the Amphion/NAIF system for generating Fortran code from high-level graphical specifications describing problems in space system geometry. Amphion/NAIF specifications describe input-output functions that compu…
Summary form only given. Given a program and a specification, you may want to verify mechanically and efficiently that this program satisfies the specification. Software verification techniques typically involve theorem proving. If a formal specification is easily available, cons…
The paper presents an approach to model checking software system designs specified in xUML (http://www.kc.com/html/xuml.html), an executable subset of UML. This approach is enabled by the execution semantics of xUML and is based on automatic translation from xUML to S/R, the inpu…
The paper proposes a novel approach to locating software components from a large component repository: context-aware browsing. Without any explicit input from software developers, this approach automatically locates and presents a list of software components that could possibly b…
Good quality models for the analysis of complex enterprise information systems (EIS) are hard to build and require lots of experience and effort, which are not always available. A possible solution to deal with the previous issue is to build automated procedures for quality model…
The use of the Unified Modelling Language (UML) during systems development has been growing in scale and complexity, often resulting in inconsistent specifications. We present a knowledge base goal-driven approach for consistency management of UML specifications represented as ax…
This paper discusses a representation for the specification of technology components exploiting the separation of domain requirements (i.e. functional, data and timing requirements) from installation requirements (i.e. implementation specific infrastructure requirements). A proce…
Testing has a vital support role in the software engineering process, but developing tests often takes significant resources. A formal specification is a repository of knowledge about a system, and a recent method uses such specifications to automatically generate complete test s…
An adaptive component is a component that is able to adapt its behavior to different execution contexts. Building an adaptive application is difficult because of component dependencies and the lack of language support. As a result, code that implements adaptation is often tangled…
Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a correct and modular way. In this pa…
A tool and techniques are presented for test data generation and identification of a path's likely unfeasibility in structural software testing. The tool is based on the dynamic technique and search using genetic algorithms. Our work introduces a new fitness function that combine…
This paper presents an architecture description language, called /spl pi/-SPACE, designed to cope with requirements on evolving software architectures. /spl pi/-SPACE provides constructs for describing architectures based on the /spl pi/-calculus. It supports the adding, replacin…