SYNTHESIZING STRUCTURED ANALYSIS AND OBJECT-BASED FORMAL SPECIFICATIONS

Structured Analysis (SA) is a widely-used software development method. SA specifications are based on Data mow Diagrams (DFD's), Data Dictio naries (DD's) and Process Specifications (P-Specs). As used in practic e, SA specifications are not formal. Seemingly orthogonal approaches t o specifications are those using formal, object-based, abstract model specification languages, e.g., VDM, Z, Larch/C++ and SPECS. These lang uages support object-based software development in that they are desig ned to specify abstract data types (ADT's). We suggest formalizing SA specifications by: (i) formally specifying flow value types as ADT's i n DD's, (ii) formally specifying P-Specs using both the assertional st yle of the aforementioned specification languages and ADT operations d efined in DD's, and (iii) adopting a formal semantics for DFD ''execut ion steps''. The resulting formalized SA specifications, DFD-SPECS, ar e well-suited to the specification of distributed or concurrent system s. We provide an example DFD-SPEC for a client-server system with a re plicated server. When synthesized with our recent results in the direc t execution of formal, model-based specifications, DFD-SPECS will also support the direct execution of specifications of concurrent or distr ibuted systems.