This post introduces Simple “Specification Driven Development” Demo as a way to adapt Formal Methods to application development, also for existing applications. Benefits can be gained immediately in Test Management of System Tests, when using formal model to generate API traces, which are mapped as unit tests on existing application, and the aggregate result of individual unit tests interpreted as an execution of a “virtual” system test – easier to that managing the system test as single unit.
An analysis section identifies several less than optimal development architecture arrangement in the demo, and points out needs for improvements.
Table of Contents
1 Introduction to Simple Specification Driven Development Demo
This chapter gives an overview of “Simple Specification Driven Development Demo” and explains desing dataflows to create virtual system test on target application.
1.1 Simple Specification Driven Development Demo Overview
“Simple Specification Driven Development Demo” is divided into three major parts:
Figure 1: Overiew of Simpole Specification Driven Development Demo
In short, the demo defines an External Schema for one scenario in an existing application, timeoff-management, and creates a Formal Model generating API Traces as executions on Formal Model. The API Traces are mapped to unit test on an implementation downloaded from a GitHub repository.
For more details refer documentation site of the demo.
1.2 Design Dataflows for Virtual System Tests
The picture below presents design dataflows in the demo to create virtual system tests on target application:
- Transformation of Logical Schema to an External Schema in Swagger format, and using it to generate Formal Interfaces in the Formal Model.
- Resolvers in a Formal Model mapping attributes in External Schema to Domains. For Formal Model execution an Environment Setup assigns Formal Data Values to Domains. The setup defines also behavior of environment in the Formal Model by giving sequence of interface calls, together with constraints of parameters bindings on Formal Data Values.
- Formal Schema being defined implicitly within specification code. A Formal Service interacts with environment using request/response messages in External Schema format, and transforms these messages into Formal Schema registering Formal State.
- Formal Model generating API traces. API Traces are sequences of API Steps with each step giving 1) Formal State of the application before an API call, 2) formal request message sent to the API, 3) expected formal response from the API call, 4) and expected Formal State of the application after the API call.
- Test Runner inputting API traces, extracting API steps for the interface to test, and creating unit tests on the implementation. Creating an unit test includes transforming Formal Schema to Physical Schema to setup persistent state of the application before an API call, and checking state of the application after the API call. Schema transformation from Formal Schema to External Schema is needed to create API request/response messages. In addition to schema transformations, Test Runner maps Formal Data Values to implementation data.
- Physical Schema being embedded within application code, separately from Schema and API Design. Application internal actions, including schema operations, are hidden from the Test Runner. Test Runner communicates with the application over user interface and accesses data base directly, instead.
Figure 2: Design Dataflows for Virtual System Tests
Design dataflows, and hyperlinks to demo documentation site, are detailed in the table below.
| Flow ID | Description |
|---|---|
| 1 | Environment makes an API call to an interface specified in Swagger Specification |
| 2 | Resolver maps interface parameters on the API call to Domains |
| 3 | Environment Setup defines values sets for Domains |
| 4 | API call executes Formal interface |
| 5 | Formal Service executes, schema transformation external => formal schema |
| 6 | Formal Service modifies Formal State. |
| 7 | A possibility operator generates API Trace execution on formal model |
| 8 | Test runner iterates API Steps in the API trace |
| 9 | Test runner set up before state, schema transformation formal => physical |
| 10 | Test runner set up before state, map data value values formal => implementation |
| 11 | Test runner set up before state |
| 12 | Test runner send API request, schema transformation formal => external |
| 13 | Test runner send API request, map data value formal => implementation |
| 14 | Test runner send API request |
| 15 | Application service executes, schema tranformation external => physical |
| 16 | Application service updates persistent state |
| 17 | Test runner receive API response and assert correctness |
| 18 | Test runner receive API response, schema transformation formal => external |
| 19 | Test runner receive API response, map data value formal => implementation |
| 20 | Test runner read after state and assert correctness |
| 21 | Test runner read after state, schema transformation formal => physical |
| 22 | Test runner read after state, map data value formal => implementation |
2 Needs for Improvement in Simple SDD Demo
This chapter identifies several less than optimal development architecture arrangement in the demo and makes suggestions for improvements
2.1 In Development Architecture
- Integrate Virtual System Testing With Existing Unit Test Frameworks
Test runner in the demo was implemented separately from application testing framework – essentially duplicating codebase for testing.
A better alternative would have Virtual System Testing to use an existing unit test framework to access the target application.
Suggestion: Implement integration for Virtual System Testing to use an existing unit test framework.
- Dispatch Virtual System Testing Value Mappers Using Resolver Configuration
Test Runner duplicates Resolver logic in code, when it chooses the right value mapper to convert Formal Data Value to Implementation Data Value in an unit test.
Suggestion. Include Resolver configuration in the API trace -file generated in Formal Modeling, and and use it to dispatch value mappers in in Virtual System Testing.
2.2 In Development Practices
- Better Support for Schema Transformations
Demo contains several schema transformations:
- Logical Schema is transformed to an External Schema (data flow #1 in the picture of chapter 1.2)
- Formal Service interacts with environment using request/response messages in External Schema format, and transforms these messages into Formal Schema registering Formal State (data flow #5)
- Test Runner transforms Formal Schema to a Physical Schema to setup service state before an API call, and to assert service state after the API call. (data flows #9, #21)
- Test Runner transforms Formal Schema to External Schema, when building an API request and processing the API response. (data flows #12, #18)
- Implementation is a black box transforming user interface to Physical Schema, and its actions within remains hidden for rest of the demo.
Suggestion: Provide tools, e.g. code generators, to help in implementing schema transformations in Schema and API Design, Formal Modeling, Virtual System Testing, and in target application implementation.
- Guideline for Schema Versioning
An article Evolutionary Database Design starts from the assumption that as the requirements cannot be fixed up-front, the application and its database need to be evolved using iterations.
Evolutionary Database Design suggests among others following practises for database schema management,
- All database artifacts are version controlled with application code
- All database changes are database refactorings. They modify the schema, but, on their own, schema changes do not change the ovewall behavior of the software.
- Clearly separate all database access code to a separate database access layer.
- All database changes are migrations identified uniquely by a sequence number. The sequence number allows tracking, which migrations have been applied to the database, and managing the sequencing constraints between the migrations.
- Everybody gets their own database instance to allow developers to work independently
- Developers continuously integrate database changes together to avoid risk of conflicting changes.
- Transition phase, supporting old and new access pattern, should be used, if destructive schema change is to be deployed. Normally, pursue non-destructive changes.
- Automate the refactorings for rolling out forward changes, with the application supporting old and new access patterns for schema changes.
- Release frequently
Suggestion: Create Guideline for Schema Versioning adapting the ideas of Evolutionary Database Desging in versioning of External Schemas, Formal Schema, and Physical Schemas.
- Support Required/Provided Component Version
Schema and API Design passes External Schema in Swagger file to Formal Modeling using a staging directory. Message buffers, such as this, may result to co-ordination problems in application components. For example, extending a system with a new attribute requires adding the attribute to External Schema, and modifying Formal Service. Modifying Formal Service, prior having a version of External Schema supporting the attribute added, creates an error in the Formal Model, and results to a failure to execute the model. Diagnosing the fault may be quite difficult, if the error goes a long way before being detected.
Suggestion: Add support to define and check consistency of required/provided component versions in the development architecture.
- Use Interface Specification both for Formal Model and Implementation
Swagger API specification in the demo generates interfaces only for the Formal Model. It is not used for the Implementation.
Suggestion: Implementation and its Formal Model should use the same interface specifications.
- Associate Domains with Attributes in Logical Schema
The demo uses resolvers to map Formal Model attribute to Domains. This association should actually be defined in Logical Schema.
The reason for this arrangement, was that Sbuilder -tool did not have an interface allowing resolvers to be imported.
Suggestion: Extend Schema and API Design to export attribut/domain association, and Sbuilder to import attribute/domain association.
2.3 In Abstracting Implementation
- Support Multiple Formal Model Abstractions
The demo specified one Formal Model generating API Traces. More generally, we would like create multiple Formal Models with different abstractions.
For example, in an refractoring scenario, we could be interested in finding all possible execution paths trough composition of services, and in verifying that some business function is executed for all the paths. In another scenario, for service architecture guaranteeing only eventual consistency of data items, we could be interested in verifying that some business constraint is not violated across application databases. Formal Service abstractions and Formal Schemas, supporting these two scenarios, may be different.
Fixing Formal Model abstraction in advance is not possible, and development architecture should allow using several Formal Models in generating API Traces.
Suggestion: Add support to define multiple Formal Model abstraction composed of Formal Schema and Formal Service
- Add Support To Test Abstract API Steps
In the demo, an API Step specified fully database setup and parameters of the API request – one API Step created one unit test on the implementation.
More realistically, steps in an API trace are abstract, i.e. some Physical Schema and External Schema attributes on the implementation are without correspondence in an API Step. Virtual system testing should allow using any value for unspecified attributes, also values, which result to service failure due to input validation.
Suggestion: Add support in to test abstract API Steps.
- Add Support To Refine Formal Models (Manually)
Normally, expect a Virtual System Test to pass and to report that ‘an Application Service correctly abstracts an API Step‘.
For system failures, a test should be reported as ‘inconclusive’ and re-executed, once the system error has been resolved.
More consideration is needed, when the failure is in ‘Application Service not abstracting API Step correctly’. Two alternatives must considered, either error is in the implementation, or the API Step is too abstract to capture implementation adequately. As the result, either fix the implementation, or refine the Formal Model.
Automatic refinement of abstract formal models is used in quality assurance of MS-Windows device drivers. In general, automatic refinement is not feasible, however, development architecture should offer the possibility to do it manually
Suggestion: Add support and guidelines to refine Formal Models (manually)
3 Fin
This blog post has used “Simple ‘Specification Driven Development’ Demo” to point out several issues, which may rise, when trying to apply Specification Driven Development for real cases. It is left for further blog post(s) to cover, how to solve these issues.
jarjuk 