Model Driven Engineering (MDE) aims to expedite the software development process by providing support for transforming models to running systems. Many modeling tools provide forward engineering features, which automatically translate a model into a skeletal program that developers must complete. Inconsistencies between a design model and its implementation, however, can arise, particularly when a final implementation is developed dependently on the code from which it was generated. Manually checking that an implementation conforms to its model is a daunting task. Thus, an MDE tool that developers can use to check that implementations conform to their models can significantly improve a developer's productivity. This paper presents a model-based approach for testing whether or not an implementation satisfies the constraints imposed by its design model. Our model-based testing approach aims to efficiently reduce the test input space while supporting branch coverage criteria. To evaluate the approach's ability to uncover inconsistencies, we developed a prototypical tool and applied it to the Eclipse UML2 projects. We were able to uncover inconsistencies between the models and their implementations using the tool.

Access control models must be analyzed to uncover flaws that can be exploited to gain unauthorized access. The UML has been used to describe access control models and there are a number of proposed approaches for analyzing UML access control models. Practical support for checking UML access control models against temporal properties is still lacking. In this paper, we describe a lightweight approach to analyzing a UML model of security policies against linear temporal properties. The access control policies are based on a generalized spatio-temporal role-based access control (GSTRBAC) model. We use a demonstration case study to show how the approach can be used to uncover access control problems.

Models are an important tool in conquering the increasing complexity of modern software systems. Key industries are strategically directing their development environments towards more extensive use of modeling techniques. This workshop sought to understand, through critical analysis, the current and future uses of models in the engineering of software-intensive systems. The MISE-workshop series has proven to be an effective forum for discussing modeling techniques from the MDD and the software engineering perspectives. An important goal of this workshop was to foster exchange between these two communities. The 2013 Modeling in Software Engineering (MiSE) workshop was held at ICSE 2013 in San Francisco, California, during May 18–19, 2013. The focus this year was analysis of successful applications of modeling techniques in specific application domains to determine how experiences can be carried over to other domains. Details are available at: https://sselab.de/lab2/public/wiki/MiSE/index.php.

Mobile applications allow individuals on-the-move access to resources "anytime, anywhere" using hand-held mobile devices. We argue that for critical and sensitive resources this is often times not desirable -- a lost or stolen mobile device can be tampered with to view or alter sensitive information. We need authorization policies that take into account time of access and location of the user in addition to the credentials of the user. Towards this end, we propose a new spatio-temporal role-based access control model. It improves upon existing models by providing features that are useful for mobile applications. Thus, an application using our model can specify different types of spatio-temporal constraints. We discuss how such an application using our spatio-temporal access control model can be verified using the UPPAAL model checker. We also demonstrate how to reduce the state-space explosion problem that is inherent in model checkers.

The Repository for Model-Driven Development (ReMoDD) contains artifacts that support Model-Driven Development (MDD) research and education. ReMoDD is collecting (1) documented MDD case studies, (2) examples of models reflecting good and bad modeling practices, (3) reference models (including metamodels) that can be used as the basis for comparing and evaluating MDD techniques, (4) generic models and transformations reflecting reusable modeling experience, (5) descriptions of modeling techniques, practices and experiences, and (6) modeling exercises and problems that can be used to develop classroom assignments and projects. ReMoDD provides a single point of access to shared artifacts reflecting high-quality MDD experience and knowledge from industry and academia. This access facilitates sharing of relevant knowledge and experience that improve MDD activities in research, education and industry.

SUMMARY Advances in communication devices and technologies are dramatically expanding our communication capabilities and enabling a wide range of multimedia communication applications. The current approach to develop communication‐intensive applications results in products that are fragmented, inflexible, and incapable of responding to changing end‐users' communication needs. These limitations have resulted in the need for a new development approach of building communication applications that are driven by end‐users and that support the dynamic nature of communication‐based collaboration. To address this need, the Communication Virtual Machine (CVM) technology has been developed to support rapid specification and automatic realization of user‐centric communication applications based on a domain‐specific modeling approach. The CVM technology consists of a domain‐specific modeling language (DSML), the Communication Modeling Language (CML), that is used to create communication models, and a semantic rich platform, the CVM, that realized the created communication models. In this paper, we report on our experiences of applying a systematic approach to engineering CML and the synthesis of CML models in CVM. Based on a feature model describing the taxonomy of the user‐centric communication domain in a network independent manner, we develop the meta‐model of CML and its different concrete syntaxes. We also present a behavioral specification (dynamic semantics) of CML that enables the dynamic synthesis of user‐centric communication models into an executable form called communication control script. We validated the CML semantics using Kermeta, a meta‐programming environment for engineering DSMLs, and evaluated the practicality of our approach using a CVM prototype and a set of experiments. Copyright © 2011 John Wiley & Sons, Ltd.

Rapid advances in electronic communication devices and technologies have resulted in a shift in the way communication applications are being developed. The emerging development strategies provide end-users with a greater ability to manipulate the underlying communication technologies by providing the appropriate level of abstraction, referred to as user-centric communication. In communication-intensive domains such as telemedicine and disaster management, the user-centric communication strategies still lack the ability to coordinate the various communication services in collaborative processes. In this paper, we present a domain-specific modeling language (DSML), Workflow Communication Modeling Language (WF-CML), that supports the rapid realization of collaborative user-centric communication applications. WF-CML is an extension of CML with communication specific abstractions of workflow concepts. To realize WF-CML models, the dynamic synthesis process in the Communication Virtual Machine (CVM) prototype was extended to coordinate the negotiation and media transfer processes based on events generated during the collaboration. We also present a comparative study to show the advantage of using WF-CML over a general-purpose workflow language and execution environment.

Feature models (FMs) are a popular formalism for describing the commonality and variability of software product lines (SPLs) in terms of features. As SPL development increasingly involves numerous large FMs, scalable modular techniques are required to manage their complexity. In this paper, we present a novel slicing technique that produces a projection of an FM, including constraints. The slicing allows SPL practitioners to find semantically meaningful decompositions of FMs and has been integrated into the FAMILIAR language.

Variability in software product lines is often expressed through feature models (FMs). To handle the complexity of increasingly larger FMs, we propose semantically meaningful decomposition support through a slicing operator. We describe how the slicing operator is integrated into the FAMILIAR environment and how it can be combined with other operators to support complex tasks over FMs in different case studies.

The use of domain-specific modeling languages (DSMLs) results in higher productivity during the development process. This is accomplished by raising the level of abstraction during design and focusing on domain concepts rather than low-level implementation details. Unlike other development paradigms, little work has been done in determining and measuring the claimed benefits of using DSMLs. In this paper, we propose a new approach to determine the effort involved in creating and using DSML models to develop applications and to manage the behavior of applications at runtime. The approach involves a classification of the effort involved, and definition of relevant metrics to measure the effort for each category. A case study is presented that shows how we applied the proposed metrics during the development and execution of an application using three different DSMLs. Categories and Subject Descriptors

There is a need for rigorous analysis techniques that developers can use to uncover security policy violations in their UML designs. There are a few UML analysis tools that can be used for this purpose, but they either rely on theorem-proving mechanisms that require sophisticated mathematical skill to use effectively, or they are based on model-checking techniques that require a ldquoclosed-worldrdquo view of the system (i.e., a system in which there are no inputs from external sources). In this paper we show how alight weight, scenario-based UML design analysis approach we developed can be used to rigorously analyze a UML design to uncover security policy violations. In the method, a UML design class model, in which security policies and operation specifications are expressed in the Object Constraint Language (OCL), is analyzed against a set of scenarios describing behaviors that adhere to and that violate security policies. The method includes a technique for generating scenarios. We illustrate how the method can be applied through an example involving role-based access control policies.

In aspect-oriented modeling (AOM), a design is described using a set of design views. It is sometimes necessary to compose the views to obtain an integrated view that can be analyzed by tools. Analysis can uncover conflicts and interactions that give rise to undesirable emergent behavior. Design models tend to have complex structures and thus manual model composition can be arduous and error- prone. Tools that automate significant parts of model composition are needed if AOM is to gain industrial acceptance. One way of providing automated support for composing models written in a particular language is to define model composition behavior in the metamodel defining the language. In this paper we show how this can be done by extending the UML metamodel with behavior describing symmetric, signature-based composition of UML model elements. We also describe an implementation of the metamodel that supports systematic composition of UML class models.

Dependable software systems are difficult to develop because developers must understand and address several interdependent and pervasive dependability concerns. Features that address pervasive dependability concerns such as error detection and recovery tend to crosscut application architecture and thus understanding and changing their descriptions can be difficult. Separating these features at the architectural level allows one to better understand and reuse them and thus can lead to better analysis and evolution of the features during design. In this paper we illustrate how an Aspect Oriented Modeling (AOM) technique can be used to model dependability aspects of component architectures separately from other aspects. The AOM architectural model used to illustrate the approach in this paper consists of a component primary view describing the base architecture and a component template aspect model describing a fault tolerance feature that provides error detection and recovery services.

Identifying and resolving design problems in the early design phase can help ensure software quality and save costs. There are currently few tools for analyzing designs expressed using the Unified Modeling Language (UML). Tools such as OCLE and USE support analysis of static structural properties. These tools provide mechanisms for checking instance models against invariant properties expressed using the object constraint language (OCL). In this paper we propose an approach to analyzing behavioral properties of UML models that can utilize static analysis tools. The approach includes a technique for generating a class model of behavior from operation specifications expressed in a restricted form of OCL Behavioral properties are expressed as invariants defined in the class model of behavior. Static analysis tools such as USE and OCLE can be used to check object models describing series of snapshots. Most of the analysis can be automated. We illustrate our approach by analyzing static separation of duty and dynamic separation of duty properties of a hierarchical role-based access control model (HRBAC).

Practical model validation techniques are needed for model driven development (MDD) techniques to succeed. This paper presents an approach to generating inputs to test UML design models that are produced in the detailed design phase of an MDD project. A symbolic execution based approach is used to derive test input constraints from the paths of a variable assignment graph, which integrates information from UML class and sequence diagrams. The constraints are solved using Alloy, a configuration constraint solver, to obtain the test inputs. The results of a pilot study carried out to explore the fault detection capability of the test inputs are reported

To manage the development of cooperative information systems that support the dynamics and mobility of modern businesses, separation of concern mechanisms and abstractions are needed. Model driven development (MDD) approaches utilize abstraction and transformation to handle complexity. In MDD, specifying transformations between models at various levels of abstraction can be a complex task. Specifying transformations for pervasive system services that are tangled with other system services is particularly difficult because the elements to be transformed are distributed across a model. This paper presents an aspect oriented model driven framework (AOMDF) that facilitates separation of pervasive services and supports their transformation across different levels of abstraction. The framework facilitates composition of pervasive services with enterprise services at various levels of abstraction. The framework is illustrated using an example in which a platform independent model of a banking service is transformed to a platform specific model.

Model driven development (MDD) tackles software complexity through the use of models. However, managing relationships and specifying transformations between models at various levels of abstraction are complex tasks. System models tangled with concerns such as security and middleware make it difficult to develop complex systems and specify model transformations. This paper presents an MDD framework that uses aspect oriented techniques to facilitate separation of concerns. We argue that using the framework will simplify both the model development task and the task of specifying transformations. The conceptual model of the framework is presented and illustrated using distributed transactions at the PIM and PSM levels.

In model driven development (MDD), specifying transformations between models at various levels of abstraction can be a complex task. Specifying transformations for pervasive system features that are tangled with other system features is particularly difficult because the elements to be transformed are distributed across a model. This paper presents an aspect oriented model driven framework (AOMDF) that facilitates separation of pervasive features and supports their transformation across different levels of abstraction. The framework is illustrated using an example in which a platform independent model of a banking application is transformed to a platform specific model.

For model driven development approaches to succeed, there is a need for model validation techniques. This paper presents an approach to testing designs described by UML class diagrams, interaction diagrams, and activity diagrams. A UML design model under test is transformed into an executable form. Test infrastructure is added to the executable form to carry out tests. During testing, object configurations are created, modified and observed. In this paper, we identify the structural and behavioral characteristics that need to be observed during testing. We describe a prototype tool that (1) transforms UML design models into executable forms with test infrastructure, (2) executes tests, and (3) reports failures.

Security critical systems must perform at the required security level, make effective use of available resources, and meet end-users expectations. Balancing these needs, and at the same time fulfilling budget and time-to-market constraints, requires developers to design and evaluate alternative security treatment strategies. In this paper, the authors presented a development framework that utilizes Bayesian belief networks (BBN) and aspect-oriented modeling (AOM) for a cost-benefit trade-off analysis of treatment strategies. AOM allows developers to model pervasive security treatments separately from other system functionality. This eases the trade-off by making it possible to swap treatment strategies in and out when computing return on security investments (RoSI). The trade-off analysis is implemented using BBN, and RoSI is computed by estimating a set of variables describing properties of a treatment strategy. RoSI for each treatment strategy is then used as input to choice of design.

Access control features are often spread across and tangled with other functionality in a design. This makes modifying and replacing these features in a design difficult. Aspect-oriented modeling (AOM) techniques can be used to support separation of access control concerns from other application design concerns. Using an AOM approach, access control features are described by aspect models and other application features are described by a primary model. Composition of aspect and primary models yields a design model in which access control features are integrated with other application features. In this paper, we present, through an example, an AOM approach that supports verifiable composition of behaviors described in access control aspect models and primary models. Given an aspect model, a primary model, and a specified property, the composition technique produces proof obligations as the behavioral descriptions in the aspect and primary models are composed. One has to discharge the proof obligations to establish that the composed model has the specified property.

Agile processes focus on the early facilitation and fast production of working code, and are based on software-development process models that support iterative, incremental development of software. Although agile methods have existed for a number of years now, answers to questions concerning the suitability of agile processes to particular software-development environments are still often based on anecdotal accounts of experiences. An appreciation of the (often unstated) assumptions underlying agile processes can lead to a better understanding of the applicability of agile processes to particular situations. Agile processes are less likely to be applicable in situations in which core assumptions do not hold. This article examines the principles and advocated practices of agile processes to identify underlying assumptions. It also identifies limitations that may arise from these assumptions and outlines how the limitations can be addressed by incorporating other software-development techniques and practices into agile development environments.

An innovative middleware-transparent approach to developing distributed applications is presented. The approach uses an aspect-oriented software development technique to separate an application's middleware-independent functionality from its middleware-specific functionality. Application elements that are specific to the middleware are localized in aspects that can be seamlessly integrated into middleware-independent application designs. The middleware-transparent approach is used to decouple business functionality from middleware-specific functionality. The decoupling allows developers to change middleware application elements without significantly modifying business functionality. Middleware technologies such as Java Remote Method Invocation (RMI), Jini, Simple Object Access Protocol (SOAP) remote procedure call (RPC) and .Net are used as examples to illustrate the approach. Copyright © 2005 John Wiley & Sons, Ltd.

The Mdel Driven Architecture (MDA) initiative formulated by the Object Management Group (OMG) is intended to support the development of software-intensive systems through the transformation of models to executable components and applications. Techniques and technologies that support rigorous definition of model transformations are required to realize the MDA vision. In this paper, we describe a technique for specifying pattern-based transformations of UML models consisting of class and interaction diagrams. The transformation specifications can be used to support systematic and verifiable transformations of UML models.

Organizations use Role-Based Access Control (RBAC) to protect information resources from unauthorized access. We propose an approach, based on the Unified Modeling Language (UML), that shows how RBAC policies can be systematically incorporated into an application design. We consider an RBAC model to be a pattern which we express using UML diagram templates; RBAC policies for an application conforming to this model can be generated by instantiating these templates with values obtained from the application. The constraints of the RBAC model are expressed using the Object Constraint Language (OCL). OCL constraints, based on first-order logic, are difficult to understand. To alleviate this problem, we show how violation of such constraints can be visually represented using object diagram templates. With adequate tool support, developers can use these to demonstrate constraint violations in their applications. Our approach is illustrated using a small banking application.

Informally described design patterns are useful for communicating proven solutions for recurring design problems to developers, but they cannot be used as compliance points against which solutions that claim to conform to the patterns are checked. Pattern specification languages that utilize mathematical notation provide the needed formality, but often at the expense of usability. We present a rigorous and practical technique for specifying pattern solutions expressed in the unified modeling language (UML). The specification technique paves the way for the development of tools that support rigorous application of design patterns to UML design models. The technique has been used to create specifications of solutions for several popular design patterns. We illustrate the use of the technique by specifying observer and visitor pattern solutions.

Design patterns describe solutions to recurring design problems in the development of software designs. To encourage the use of design patterns, we are investigating tool support for incorporating patterns into UML models. The development of such tools requires patterns to be specified at the metamodel level. Patterns may be specified using roles, where a role is played by model elements. However, the notion of role in the object-oriented community is strictly based on objects, and does not allow the use of the word "role" in any other place where the context is not object-based. In this paper, we propose a notion of role that can be used to specify design patterns at the metamodel level. We survey the characteristics of object-based roles and generalize them. Based on the generalized notion of a role define a new notion of a model role which is played by a model element. We illustrate the use of model roles with a specification of a variant of the Observer design pattern.

Systematic design testing, in which executable models of behaviors are tested using inputs that exercise scenarios, can help reveal flaws in designs before they are implemented in code. We present a testing method in which executable forms of the Unified Modeling Language (UML) models are tested. The method incorporates the use of test adequacy criteria based on UML model elements in class diagrams and interaction diagrams. Class diagram criteria are used to determine the object configurations on which tests are run while interaction diagram criteria are used to determine the sequences of messages that should be tested. The criteria can be used to define test objectives for UML designs. In this paper, we describe and illustrate the use of the proposed test method and adequacy criteria.

Abstract Systematic design testing, in which executable models of behaviours are tested using inputs that exercise scenarios, can help reveal flaws in designs before they are implemented in code. In this paper a technique for testing executable forms of UML (Unified Modelling Language) models is described and test adequacy criteria based on UML model elements are proposed. The criteria can be used to define test objectives for UML designs. The UML design test criteria are based on the same premise underlying code test criteria: coverage of relevant building blocks of models is highly likely to uncover faults. The test adequacy criteria proposed in this paper are based on building blocks for UML class and interaction diagrams. Class diagram criteria are used to determine the object configurations on which tests are run, while interaction diagram criteria are used to determine the sequences of messages that should be tested. Copyright © 2003 John Wiley & Sons, Ltd.

Developers of complex systems have to address concerns such as security, availability of services, and timeliness that often are non-orthogonal to traditional design structures, that is, the concerns cross-cut traditional design units. We illustrate how an aspect-oriented approach to modeling allows developers to encapsulate such design concerns so that they can be woven into a design in a systematic and consistent manner. The paper focuses on the use of aspects for modeling and weaving in security concerns.

Cost-effective development of large, integrated computer-based systems can be realized through systematic reuse of development experiences throughout the development process. We describe a technique for representing reusable modeling experiences. The technique allows developers to express domain-specific design patterns as a sub-language of the modeling language, the UML. Use of the sub-language to build application-specific UML models results in the reuse of the embedded design experiences. We use a notation called the (meta)Role-Based Modeling Language (RBML) to define UML sub-languages. A (meta-)Role Model is a specialization of the UML (Unified Modeling Language) meta-model, that is, it determines a sub-language of the UML. We show how RBML can be used to define domain-specific design patterns.

It is well-known that uncontrolled change to software can lead to increasing evolution costs caused by deteriorating structure and compromised system qualities. For complex systems, the need to carefully manage system evolution is critical. In this paper we outline an approach to managing evolution of object-oriented (OO) software. The approach is based on a goal-directed, cyclic process, in which OO models are transformed and quantitatively evaluated in each cycle. Evaluation criteria guide developers in choosing between alternative transformations in each cycle. The process, transformations, and evaluation techniques can be used to develop systems from a set of baseline models.

Summary form only given. The authors are currently developing a model-driven, repository-based approach to system evolution management. The primary domain of interest is the telecommunication IT system area, but the techniques are applicable to organizations with integrated systems of systems. The approach is model-driven in the sense that data and object-oriented (OO) models (expressed in the Unified Modeling Language (UML)) are used to represent system implementations at various levels of abstractions (business requirements, system requirements, logical and physical design).

The Fusion and Syntropy object-oriented methods reflect some of the most rigorous object-oriented modelling concepts and experiences currently available. In this paper we identify similarities and differences between the two methods, and discuss how the best concepts from each of these methods can be combined to obtain clearer, more precise analysis models, specifications, and designs, and can be used to enhance the modelling power of the other. A summary of a semantics for Syntropy is given in Appendix A, and ways in which this can be extended to Fusion are described. This work was carried out as part of the EPSRC projects ‘Object-oriented Specification of Reactive and Real-time Systems’ concerning the extension of Fusion to treat reactive systems, and ‘Formal Underpinnings for Object Technology’ concerned with developing a full semantics for Syntropy.

Black-box test-generation requires a model of the system under test to describe what is to be tested. Testing criteria and test objectives define how it is to be tested. This paper describes an approach to black-box test-generation in which an AI (artificial intelligence) planner is used to generate test cases from test objectives derived from UML (Unified Modeling Language) Class Diagrams. The UML Class Diagrams are conceptual models of the systems under test. They differ from traditional design and requirements models in that they include information pertinent to test case generation. From these models, test objectives and a domain theory are: obtained, transformed to planner representations, and input to the planner. The planner uses the problem description to generate a test suite that satisfies the UML-derived test objectives. This paper describes the application of the testing approach to an industrial problem.

This paper introduces a denotational semantics for a core of the draft IEEE standard analog and mixed signal design language VHDL-AMS, and derives general results about the behaviour of VHDL-AMS programs from it. We include, for example, a demonstration that VHDL-AMS parallelism is benign in the absence of shared initializations. As proof of concept we have built an interpreted simulator that prototypes the semantics and which runs multi-process mixed analog and digital descriptions correctly.

Black box test generation needs a model of the system under test to describe what is to be tested. Testing criteria and test objectives define how it is to be tested. We explain how to represent a system under test via UML models. We derive test objectives from the UML models and use the objectives and the models to generate test cases by mapping them into a problem description for an AI planner. The planner uses the problem description to generate a test suite that satisfies the UML-derived test objectives.

The Unified Modeling Language (UML) is a standard modeling language in which some of the best object-oriented (OO) modeling experiences are embedded. In this paper we illustrate the role formal specification techniques can play in developing a precise semantics for the UML. We present a precise characterization of requirements-level (problem-oriented) Class Diagrams and outline how the characterization can be used to semantically analyze requirements Class Diagrams.

There is much interest in developing a firm semantic base for object-oriented modeling concepts. By providing precise characterizations of object-oriented (OO) modeling concepts one gains the ability to build a precise OO model of behavior and structure that can be rigorously analyzed. We present the current results of our ongoing formalization of the Unified Modeling Language (UML). UML is a proposed common OO modeling language, thus it is important that it has a formally defined semantic base. The focus of this paper is the formalization of the primary UML constructs used to build class structures. We use the Z notation to precisely express the meaning of UML class structures.

We present techniques for constructing Z specifications from the analysis and design models of the Fusion method. We show how the specifications can be used to more closely tie the Fusion models together. In particular, we outline how the specifications can be used to support rigorous verification of Fusion design models against analysis models.

Despite their strengths, object-oriented methods (OOMs) and their supporting CASE tools often do not produce model that are amenable to rigorous semantic analysis. This is a direct result of their loosely defined semantics. The authors outline their ongoing work on providing a semantic base for OOMs.

The difficult task of developing safety-critical systems requires the use of methods and tools that allow developers to manage inherent complexity and to meticulously specify, implement, and analyze desired behavior. Development environments based on formal specification techniques supported by CASE tools can facilitate quality development of such systems. We present our proposed environment for the development of high-assurance systems. The environment provides CASE support for developing and analyzing graphical and formal representations of system structure and behavior. We illustrate the use of the environment with a traffic control system.

The complex and critical nature of real-time, dependable systems (henceforth referred to as RTD systems) necessitates the use of analyzable specifications and specification analysis techniques supporting the assessment of behavioral, safety-critical, security, and fault-tolerant qualities of systems. The need to rigorously state and analyze RTD system specifications suggests the use of formal specification techniques (FSTs), that is techniques that provide a precise specification language and specification analysis mechanisms based on formal reasoning systems. Unfortunately, most current FSTs focus on specifying functionality, and neglect non-functional qualities such as fault tolerance and security. While there is much research on extending FSTs so that they can be applied to non-functional properties, little work has gone into developing integrated sets of FSTs that can be applied throughout the development of RTD systems. We discuss how FSTs can be utilized in a multilevel description of RTD systems. FST's make possible rigorous analysis at each level and rigorous consistency check across the levels.

The last decade has seen a large increase in the use of ‘structured’ methods of software development. They grew out of their predecessors, which consisted of a toolkit of techniques with little method of how and when to apply them. Methods such as Yourdon Structured Analysis1 and SSADM2 provide means of managing the complexity of large systems. They provide techniques and associated procedures for the development of such systems. In parallel with this, and almost entirely independently, formal specification languages and methods have been developed. Both approaches have their strengths and weaknesses. Recently it has been recognised that benefits can be gained from integrating the two. A number of researchers have reported progress towards the successful integration of formal and structured methods. This paper reports on a selection of this work. The aim in each case has been to develop specifications which are both structured and formal, and so combine the proven advantages of both approaches. We believe that such integrated methods remove some of the ‘culture shock’ associated with the introduction of mathematically formal languages, and make their use more acceptable to managers and engineers in software development organisations. There is some evidence for the feasibility and cost-effectiveness of this approach when used in an industrial setting; developers at Rolls Royce Associates3 have reported the successful combined use of VDM and Yourdon. Work has also started on the integration of formal notations and graphical techniques for Object-Oriented Analysis and Design, but this is all at a very early stage and little has been reported formally.

A method for associating a dataflow diagram (DFD) with a formal specification is described. The intention is to enhance the use of the DFD as a formal specification tool, thus gaining a tool that can be used to document application functionality in an understandable manner and, at the same time, be capable of producing a formal specification that can be used to rigorously investigate the semantic properties of the application. It is shown how the formal specifications characterizing semantic models of DFDs can be used to investigate desired application properties of verify semantic decompositions of data transforms.>