Evolving Specification Engineering

Abstract. The motivation for this work is to support a natural separation of concerns during formal system development. In a developmentby-refinement context, we would like to be able to first treat basic functionality and normal-case behavior, and then later add in complicating factors such as physical limitations (memory, time, bandwidth, hardware reliability, and so on) and security concerns. Handling these complicating factors often does not result in a refinement, since safety or liveness properties may not be preserved. We extend our earlier work on evolving specifications (1) to allow the preservation of both safety and liveness properties under refinement, and (2) to explore a more general notion of

• Type: Conference
• Year: 2008
• Where: AMAST
• Authors: Dusko Pavlovic, Peter Pepper, Douglas R. Smith
• Keywords: AMAST 2008, Liveness Properties, Natural Separation, Software Engineering, Treat Basic Functionality