Synthesizing structured analysis and object‐based formal specifications

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.