Next Generation Software Development
Abstract
Under this grant we have studied the development of a scientifically sound basis for software development that builds on widely used pragmatic methods but is firmly grounded in well-established formal domains such as first- order logic and automata theory. To be sufficiently expressive for software systems, the work has focused on methods applicable to infinite-state systems. Traditionally methods for infinite-state systems have been expensive, because they were mainly deductive and thus required guidance by users who were both experts in the application domain and in the verification methodology. Our research has been directed at algorithmic-deductive techniques that separate the combinatorial reasoning from reasoning about the data. These methods often limit user input to providing abstract system models and application-level guidance, making the interaction more natural to software developers. Constructed proofs hide low-level details; instead, they reason at the most appropriate level of abstraction with respect to the properties to be proved. This characteristic of proofs make them suitable as system documentation that can evolve with the system. To ensure well-defined semantics, computational models were developed for new computing paradigms, including aspects of publish-subscribe systems and middleware design patterns.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2005
- Accession Number
- ADA435087
Entities
People
- Zohar Manna
Organizations
- Stanford University