Abstract
The paper presents a way to incrementally introduce formal methods into the industrial practice of system development on the basis of loose specifications. Key idea is to enrich traditional and accepted design and development tools with a means for constraint-like specification, tailored to express vital frame or correctness conditions, and with an automated verification procedure guaranteeing that the specifications are met. This approach still supports the completely traditional design, but it invites to successively add constraints in order to incrementally improve the development tool with low cost: being fully automatic, the verification procedure does not require any interaction, and it provides feedback that can be understood on the application level.
| Original language | English |
|---|---|
| Pages (from-to) | 78-91 |
| Number of pages | 14 |
| Journal | Software-Concepts and Tools |
| Volume | 17 |
| Issue number | 2 |
| Publication status | Published - 1996 |
| Externally published | Yes |
Keywords
- Abstract views
- Formal methods
- Hypertext
- Incremental development of tools
- Intelligent Networks
- Large grain software engineering
- Model checking
- Service Creation Environment
- Software reuse
- Symbolic execution
- Verification