3,458 papers · page 166 of 173
The paper describes efforts that have made to mechanise the requirements engineering process in an industrial avionics domain. The authors' approach is based on an analysis of both the application domain and the task domain. The paper describes the processes they have used for do…
Persistent data often has a long lifetime. During its lifetime, the types that are used to structure the data may undergo evolution to support new requirements or provide more efficient services. This evolution often makes the persistent data inaccessible unless it also evolves w…
Although the formal method VDM has been in existence since the 1970s, there are still no satisfactory tools to support verification in VDM. The paper deals with one possible means of approaching this problem by using the PVS theorem-prover. It describes a translation of a VDM-SL …
Flexibility is recognized as a key feature in structuring software, and many architectures have been designed to that effect. However, they often come with performance and code size overhead, resulting in a flexibility vs. efficiency dilemma. The source of inefficiency in softwar…
Strategies of the structural synthesis of programs (SSP) of a deductive program synthesis method which is suited for compositional programming in large and is in practical use in a number of programming environments are outlined. SSP is based on a decidable logical calculus where…
In software testing, it is often desirable to find test inputs that exercise specific program features. To find these inputs by hand is extremely time-consuming, especially when the software is complex. Therefore, numerous attempts have been made to automate the process. Random t…
Discusses our approach to the problem of refining high-level simulation specifications. Our domain is simulated combat training for tank platoon members. Our input is a high-level specification for a training scenario and our output is an executable specification for the behavior…
This paper relates the formal specification and verification of a consensual decision protocol based on Co/sub 4/, a computer environment dedicated to the building of a distributed knowledge base. This protocol has been specified in the ISO formal description technique LOTOS. The…
Scaling formal methods to large, complex systems requires methods of modeling systems at high levels of abstraction. In this paper, we describe such a method for specifying system requirements at the software architecture level. An architecture represents a way breaking down a sy…
Because software specifications often serve as a formal contract between the developer and the customer, systems have been proposed that help the software client better understand specifications by automatically paraphrasing them in natural language. The REVIEW system applies nat…
Legacy software systems present a high level of entropy combined with imprecise documentation. This makes their maintenance more difficult, more time consuming, and costlier. In order to address these issues, many organizations have been migrating their legacy systems to new tech…
Deduction-based software component retrieval uses pre- and postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very simple but the vast number of arising proof tasks makes a practical implementation ve…
This paper presents an overview of a distributed embedded system design assistant called Systems Engineers Workbench (SEW 2.0). SEW 2.0 uses a suite of design frameworks, with supporting representations, to structure the inherent complexity. A set of design assist operatives furt…
Plan synthesis approaches in AI fall into two categories: domain-independent and domain-dependent. The domain-independent approaches are applicable across a variety of domains, but may not be very efficient in any one given domain. The domain-dependent approaches can be very effi…
A successful design of an interactive system requires a clear understanding of human-machine interaction. For the specification of such a system a precise consideration of the user's context during each step of the development process is therefore necessary. Moreover, a formal sp…
This paper presents a methodology for extracting objects from legacy imperative code. The parameter-based object identification (PBOI) methodology is based on the thesis that object attributes manifest themselves as data items passed from subprogram to subprogram in the imperativ…
Visual development environments have provided good support in the reuse of graphical user interface, report and query generation, and simpler database retrieval and updating. However, many commonly used components for computation and database processing and updating are still req…
This paper proposes a concept named unit repeated inheritance (URI) in Z notation to realize object-oriented testing of an inheritance hierarchy. Based on this unit, an inheritance level technique (ILT) method as a guide to test object-oriented software errors in the inheritance …
Program understanding efforts by individual maintainers are dominated by a process known as discovery, which is characterized by low-level searches through the source code and documentation to obtain information that is important to the maintenance task. Discovery is complicated …
This paper briefly describes our initial experiences in applied research of formal approaches to the generation and maintenance of software systems supporting structural engineering tasks. We describe the business context giving rise to this activity, and give an example of the t…