3,458 papers · page 160 of 173
Defining domain-specific abstractions for generator systems leads to a quandary between choosing abstractions that exhibit powerful programming amplification through the combinatorial opportunities provided by composition, and choosing abstractions that can be easily transformed …
The Unified Modeling Language (UML) is fast becoming an industry standard for object-oriented modeling and analysis. Applying the UML to model, analyze and design dependable systems require methods and tools for model checking that are integrated with the UML and its support envi…
In mission critical applications of distributed information systems, autonomous information resources are coordinated to meet the information demands of client specific decision-support views. The current approach to view coordination relies on design-time trade-offs to select a …
Test data generation and test execution are both time-consuming activities when done manually. Automated testing methods promise to save a great deal of human effort. This especially applies to reactive programs which have complex behaviour over time and which require long test s…
A cryptographic protocol is a short series of message exchanges, usually involving encryption, intended to establish secure communication over an insecure network. A protocol fails if an active wiretapper can obtain confidential information or impersonate a legitimate user, witho…
As software systems become larger and more complex, a relevant part of code shifts from the application domain to the management of the system's run-time architecture (e.g., substituting components and connectors for run-time automated tuning). We propose a novel design approach …
A key problem in component-based software development (CBSD) is that developers have incomplete knowledge of components. In many cases, the only available source of such information is experimentation. In this paper we argue that the provision of tool support for automated and re…
Compares our linear programming technology for software verification (LPV) with other verification systems: explicit exploration using partial order reduction (Spin) and implicit exploration using BDDs (Xeve/Esterel). The case study is a safety property of an easily-scalable prob…
A major emphasis in software development is placed on identifying and reconciling architectural and design mismatches. These mismatches happen during software development on two levels: while composing system components (e.g. COTS or in-house developed) and while reconciling view…
We describe the formal specification and automated synthesis of a strategic airlift scheduler for the Air Mobility Command of the US Air Force. The program synthesis system, the Kestrel Interactive Development System, composes a formal domain theory with a formal description of a…
There is a trend towards the increased use of automation in V&V (verification and validation). Automation can yield savings in time and effort. For critical systems, where thorough V&V is required, these savings can be substantial. We describe a progression from pilot studies to …
We address the problem of automatically verifying properties of modules written in the C/sup --/ language, a very simple imperative language. We develop a framework for automatically proving properties of modules written in C/sup --/. Our approach consists of two steps. At the fi…
Deductive retrieval and deductive synthesis are two conceptually closely related software development methods which apply theorem proving techniques to support the construction of correct programs. In this paper, we describe an integration of both methods which combines their com…
Many domain specialists are not familiar or comfortable with formal notations and formal tools like theorem provers or model generators. To address this problem, we developed Attempto Controlled English (ACE), a subset of English that can be unambiguously translated into first-or…
Constraint programming is an emerging technology that offers an original approach allowing for efficient and flexible solving of complex problems. Its main advantage relies in its ability to compute with partial information expressed in terms of constraints. These constraints are…
A number of approaches have been proposed to automatically generate test data to traverse a given path in a program. We present a program execution based approach to generate test data for a given path. The technique derives a desired input for a test path by iteratively refining…
There is a continuing need for software engineers to design better-quality systems more quickly. Component-based technologies promise to make this possible, but modern systems are too complex for a full analysis of their behaviour to be practical. We propose that a reasonable alt…
Advanced users often find themselves restricted by the limited facilities of most UML CASE tools when they want to do complex manipulations of UML models, e.g., apply design patterns, generate code for simulation and validation etc. We describe UMLAUT, a freely available UML tran…
This paper presents results of a joint case study of Ericsson and the German cellular network provider Mannesmann Mobilfunk, targeted at automating type acceptance tests. Faced with a growing number of tests required to verify the quality of the telecom switch software, both comp…
A novel approach for automatic software test generation is presented, which combines ideas from structural and functional testing as well as formal verification methods. It involves as an intermediate step, the construction of graphs and refinement types, which can be regarded as…