3,458 papers · page 159 of 173
We describe a test sequence generation method from LUSTRE descriptions and its companion tool, GATEL. The LUSTRE language is declarative and describes synchronous data-flow computations. It is used for reactive control/command systems, mainly for electrical power production appli…
Describes the formal specification and development of a separation kernel. The Mathematically Analyzed Separation Kernel (MASK), has been used by Motorola on a smartcard project, and as part of a hardware cryptographic platform called the Advanced INFOSEC (INFOrmation SECurity) M…
When a lack of data inhibits decision-making, large-scale what-if queries can be conducted over the uncertain parameter ranges. Such queries can generate an overwhelming amount of data. We describe a general method for understanding that data. Large-scale what-if queries can guid…
The synthesis of programs, as well as other synthetic tasks, often ends up with an unprovable, partially false conjecture. A successful subsequent synthesis attempt depends on determining why the conjecture is faulty and how it can be corrected. Hence, it is highly desirable to h…
Software development includes gathering information about tasks, work practices and design options from users. Traditionally requirements gathering takes two forms. Interviews and participatory design (PD) practices gather rich information about the task and the domain but requir…
Develops a domain engineering approach and the supporting tools to define software product lines. The approach is composed of a process and a notation. The notation is an extension of UML (Unified Modeling Language), while the process is influenced by the Synthesis and FAST domai…
Automated database design tools employ knowledge-based systems technology in order to provide intelligent support to humans during the process of database analysis and design. However, the level to which these tools can simulate the diagnostic capabilities of human designers when…
This paper presents the advantages and disadvantages of automatic code generation of safety critical software. It discusses three broad approaches to its generation in the context of the high levels of assurance required. Finally a number of issues that commercial tool vendors mu…
This paper presents initial results in model checking multi-threaded Java programs. Java programs are translated into the SAL (Symbolic Analysis Laboratory) intermediate language, which supports dynamic constructs such as object instantiations and thread call stacks. The SAL mode…
Although new peripheral devices are emerging at a frantic pace and require the fast release of drivers, little progress has been made to improve the development of such device drivers. Too often, this development consists of decoding hardware intricacies, based on inaccurate docu…
Many sources agree that managing the evolution of an OO system constitutes a complex and resource-consuming task. This is particularly true for reusable class libraries, as the user interface must be preserved to allow for version compatibility. Thus, the symptomatic detection of…
Consistency enforcement aims at modifying a program specification such that the result is consistent with respect to a specified set of invariants. Our approach requires the modified program specification to be a maximal consistent diminution of the original one with respect to s…
Design patterns offer many advantages for software development, but can introduce inefficiency into the final program. Program specialization can eliminate such overheads, but is most effective when targeted by the user to specific bottlenecks. Consequently, we propose that these…
Presents a group critic system for object-oriented analysis and design. A group critic system is a critiquing system which is aware that the problems it finds in the design are the result of different users acting on different goals, and all are responsible for the problem. The e…
This paper concerns automated analysis of the meaning or semantics of scientific and engineering code. The procedure involves taking a user's existing code, adding semantic declarations for some primitive variables, and automatically identifying formulae. Parsers encode domain kn…
The majority of the work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers and model checkers. In t…
Little-JIL, a new language for programming the coordination of agents, is an executable, high-level process programming language with a formal (yet graphical) syntax and rigorously defined operational semantics. Little-JIL is based on two main hypotheses. The first is that the sp…
We propose that design patterns be systematically analyzed and reformulated to exhibit a reasoning binding solutions to precisely stated problems, given a set of mechanisms. We show that these mechanisms can be described as program transformations and how an assistant tool could …
Scenarios are valuable for supporting communication among system developers in the initial phases of requirements engineering. But the problem of how to fruitfully deal with large informal or semi-formal scenario collections consisting of weakly structured texts is still a key re…
In this paper an automatic and optimized technique for test generation for communication protocol control and data portion is described, the goal is to minimize the number of tests with a guaranteed coverage. The test generation algorithm is applied to the client layer part of th…