Synthesizing structured analysis and object-based formal specifications

Abstract

Structured Analysis (SA) is a widely-used software development method. SA specifications are based on Data Flow Diagrams (DFD's), Data Dictionaries (DD's) and Process Specifications (P-Specs). As used in practice, SA specifications are not formal. Seemingly orthogonal approaches to specifications are those using formal, object-based, abstract model specification languages, e.g., VDM, Z, Larch/C++ and SPECS. These languages support object-based software development in that they are designed to specify abstract data types (ADT's). We suggest formalizing SA specifications by: (i) formally specifying flow value types as ADT's in DD's, (ii) formally specifying P-Specs using both the assertional style of the aforementioned specification languages and ADT operations defined in DD's, and (iii) adopting a formal semantics for DFD "execution steps". The resulting formalized SA specifications, DFD-SPECS, are well-suited to the specification of distributed or concurrent systems. We provide an example DFD-SPEC for a client-server system with a replicated server. When synthesized with our recent results in the direct execution of formal, model-based specifications, DFD-SPECS will also support the direct execution of specifications of concurrent or distributed systems.