DevFemOps: enhancing maintainability based on microservices using formal engineering methods

Abstract

How can we make software services evolve safely and be long-lived? By designing on the premise of microservices, the services become loosely coupled, which can localise the changes in the system and accelerate the changes. However, from a medium- to long-term perspective, it is not easy to respond to changes in technology trends, business changes including legal revisions, and changes in user requirements among the changing project members. We propose DevFemOps as a way to enhance maintainability and achieve continuous quality improvement, coining the term DevFemOps to place Formal Engineering Methods at the center of the DevOps cycle. We also define the DevFemOps QA engineer as a new role within the agile development squad that is responsible for the quality of the product. In this paper, we will describe how the DevOps cycle, with QA engineers at the center, can bring us closer to the goal of DevFemOps.

KEYWORDS:

• Formal methods
• formal engineering methods
• microservices
• agile development
• devops

Introduction

In the rapidly changing business world, it is necessary to shorten the time to market for new products and services. In the same way, services based on software need to be released to the market quickly and be able to respond to changes quickly in order to differentiate themselves from other products. However, we also need to assure the high quality of the software and improve its maintainability as a failure caused by the software operation can have catastrophic consequences, including property damage, financial loss, serious injury, or even human casualty. (Wong et al., 2017) (Wong et al., 2010) By practicing Agile Software Development Methodology (Eckstein, 2004), Agile Development, it is possible to quickly release a product to the market from the stage where some of its functions have been implemented. DevOps has been heralded as a novel paradigm to overcome the traditional boundaries between IT Development (Dev) and IT Operations (Ops) teams aiming to improve collaboration between these teams. It represents a change in IT culture, focusing on rapid IT service delivery through the adoption of agile, lean practices in the context of a system-oriented approach (Teixeira et al., 2020) (Kim et al., 2016). By running the DevOps cycle, it is possible to apply the knowledge gained from operations to the next stage of development. Furthermore, by designing on the premise of microservices, the services are loosely coupled, which localises system changes and accelerates the change speed.

It may be possible to respond quickly to changes if we keep running the DevOps cycle by the same members. However, when considering changes that will occur over the medium to long term, the engineers in the cycle could be changed and not all of them could understand the user requirements and the existing system well enough in changes such as technological trends, business changes including legal changes, and changes in user requirements. In such a changing environment, how can we ensure that software services can evolve safely and be long-lasting?

We propose DevFemOps as a way to increase ease of maintenance and achieve continuous quality improvement, coining the term DevFemOps, which places Formal Engineering Methods at the center of the DevOps cycle. In other words, integrate Formal Engineering Methods with DevOps approaches and propose a practical approach on how the DevOps cycle, starting from Formal Engineering Methods, can keep consistency between Formal Specification and implementation, and contribute to ease of maintenance and continuous quality improvement even from a mid- to long-term perspective. We also define the DevFemOps QA engineer as a new role within the agile development squad that is responsible for the quality of the product. In this paper, we describe how the DevOps cycle, with QA engineers at the center, can be rotated using SOFL (Structured Object-Oriented Formal Language) (Liu, 2004), one of the formal engineering methods, to get closer to the goal of DevFemOps.

In this paper, we first introduce DevOps, Microservices, Formal Methods, Formal Engineering Methods and one of its methods, SOFL, as background. Then, we explore the maintainability and refactoring as one of the ways to improve maintainability. Based on these, we introduce our proposal DevFemOps and explain how it can contribute to improve maintainability and continuous quality improvement.

Refactoring is performed on existing software code, whereas our approach focuses on formal specification descriptions, which can contribute to ease of maintenance even before the code is implemented. While refactoring targets code that describes how things behave, or “how” they are realised, formal specification descriptions describe the user's functional requirements, or “what,” and thus we believe that can be used better as a platform to design Microservice architectures and domain-driven design. With the proposal unified approach, we think we can provide a consistent way to improve maintainability and continuous quality improvement.

Background

Devops

DevOps is a practical method that aims to develop, test, and release IT systems quickly and frequently through collaboration between development and operations teams (Tarusawa et al., 2021). In some cases, it may be necessary to change the team structure with organisational changes.

To focus on the technical aspects, DevOps uses agile development for rapid, high-frequency development. With agile development, a product (software service) can be released to the market quickly, starting from the stage where some functions are implemented. In addition, a deployment pipeline, which is a tool to automate compilation, build, testing, and deployment, is used to ensure smooth collaboration with the operations team. Through continuous monitoring, the team can apply the knowledge gained from operations to the next stage of development.

In agile development, we can learn from the results of iterative and quick verification with working software to produce better results (IPA, 2021). In the early stages of development, the process is likely to run well with users and developers who share the same goals. On the other hand, from a mid- to long-term perspective, the number of engineers that can be deployed may increase or decrease in reality, and not all of them may have sufficient understanding of the user requirements and the existing system. In such an environment, it is not easy to make software services long-lasting while evolving them safely.

Microservices

The core of the microservices architecture is a software structure in which multiple independently developed and running software components, called services, are combined to form a single application (Fowler & Lewis, 2014) (Tarusawa et al., 2021). Technologies to realise this include containers, orchestration, REST and messaging, and the methodologies DevOps, agile development process, continuous delivery, and domain-driven design. Together, we use these technologies around the architecture and form the architectural style of microservices.

The advantages of applying microservices include the following points:

1. Fine-grained release of applications.

2. Quick and flexible application modification and maintenance.

3. Fine-grained scaling

4. Minimising the impact of failures

5. Basis for continuous delivery

Designing on the premise of microservices makes the services loosely coupled, which localises the changes in the system and speeds up the change rate. If the team is specialised in the traditional Web 3-tier structure such as user interface, application server, and DB, it is necessary to communicate and coordinate changes across teams when any changes are made. If teams are organised for each service, as in Team Service 1 in Figure 1, there is no need to communicate with other teams when changing something in Service 1.

Figure 1. Structures in microservices.

Formal methods

In software development, formal methods are one of the techniques to improve the quality of software development. Formal methods consist of formal specification descriptions and formal proofs. Formal specification descriptions use set theory and logic to describe software specifications, so that functional requirements can be described without ambiguity. First, we can write a formal specification with a high level of abstraction, and then increase the explicitness of the specification through a process of refinement. Formal proofs are used to guarantee that there are no contradictions in the specifications at a certain stage, and that the refinement process has been carried out correctly.

Formal engineering methods and sOFL

Formal Engineering Methods, FEM for short, are the methods that support the application of formal methods to the development of large-scale computer systems. Formal engineering methods are equivalent neither to application of formal methods, nor to formal methods themselves. They are intended to serve as bridge between formal methods and their applications, providing methods are related techniques to incorporate formal methods into the entire software engineering process. (Liu, 2004)

SOFL, standing for Structured Object-Oriented Formal Language, is one of the formal engineering methods, which integrates data flow diagram with Petri net semantics and formal specification description VDM-SL, and also incorporates the ideas of stepwise refinement and object orientation. (Liu, 2004) (Fukuzaki, 2000)

The structure of SOFL consists of a module and a Condition Data Flow Diagram (CDFD) as shown in Figure 2. module defines abstract data types, describes processes that describe conditions to be satisfied when a module performs an operation, and describes decompositions of processes to realise structured techniques. A process uses predicate logic expressions that indicate preconditions and postconditions as input/output specifications and operation specifications of abstract data types. CDFD is an extended version of dataflow diagram, which can describe the relationship between processes described in a module using dataflow such as selection and repetition.

Figure 2. SOFL structure (module and CDFD).

Maintainability

E. Burton Swanson (Burton Swanson, 1976) stated there are three bases of software maintenance, Corrective, Adaptive and Perfective maintenances. The Maintainability is a part of Perfective maintenance. An improvement in program maintainability is understood here to mean that the program will be more easily modified when it must be modified.

One of the techniques to improve the program maintainability is Refactoring (Thoughtworks, 2018). Refactoring is the process of improving the internal structure of software code without drastically changing its behavior. It is a disciplined method of refining code (and modifying/simplifying the internal design) to minimise the occurrence of defects. This is the process of improving the design by restructuring the code after it has been written. (Fowler, 2018)

Devfemops

We propose DevFemOps as a way to increase maintainability and achieve continuous quality improvement. DevFemOps is a term coined to place formal engineering methods at the center of the DevOps cycle, and is defined as having the following characteristics (Figure 3).

1. User requirements are expressed as formal specification descriptions (A)

2. One-to-one correspondence between formal specification and each component of implementation (B)

3. Applying domain-driven design to formal specifications based on the premise of microservices (C)

4. Refactoring of formal specifications based on the premise of microservices (D)

5. Design RESTful API design in the specification stage assuming microservices (E)

6. Quality improvement through formal specification testing and the use of test cases in program testing (F)

7. Version control of both formal specification and implementation (G)

8. Management of libraries used in implementation at the specification stage (H)

9. Changes from the formal specification (I)

10. Continuous monitoring (J)

Figure 3. Characteristics of DevFemOps.

We also define the DevFemOps QA Engineer (QA Engineer) as a new role within the agile development squad that is responsible for the quality of the product (Figure 4). We will describe how the DevOps cycle, with the QA engineer at the center, can bring us closer to the goal of DevFemOps.

Figure 4. DevFemOps QA engineer.

User requirements are expressed as formal specification descriptions

The QA engineer clarifies the user requirements through dialogues with users and product owners, and describes them as formal specifications. In addition, the QA engineer discovers ambiguous parts of the requirements while writing the formal specification, and refines the formal specification through further dialogue using concrete examples. At the same time, the QA engineer communicates the requirements to the developers through dialogues with them, and refines the formal specification from the implemented software.

In this paper, we adopt SOFL's module as the formal specification description, and represent the relationship between each process in the module by CDFD.

One-to-one correspondence between formal specification and each component of implementation

The QA engineer interacts with the developer to make sure that there is a one-to-one correspondence between each component in the formal specification and each component in the implementation. (Figure 5) For example, a module in SOFL and the processes contained in it are mapped to classes and methods in the implementation in an object-oriented manner.

Figure 5. One-to-one correspondence.

In this way, when some analysis of the implementation is required, the expected requirements can be confirmed by referring to the CDFD of the SOFL specification to see the relationship between each class, and by checking the module and process.

Applying domain-driven design to formal specifications based on the premise of microservices

The key to how each microservice is extracted is domain driven design (Evans & Imazeki, 2011). Domain analysis and service modeling are performed on the CDFD and modules of SOFL, and QA engineers work with domain specialists to understand the language of the target domain through user interaction, and adopt it as the module name, process name and type name of SOFL. We can focus on the business logic. The related business data and business logic are combined as a domain object and represented as a module. When business logic is designed as multiple processes, the relationship between them is represented by CDFD.

Refactoring of formal specifications based on the premise of microservices

In order to enhance the loosely coupled nature of microservices and to make each microservice more accessible, we perform refactoring of the formal specification.

For example, if the data store is read/written from multiple processes in CDFD, and the processes span microservices, the data store should be accessed only from within one microservice. For example, if there is a reference relationship between multiple processes and a certain process, and there is a duplication of logic in the referencing process, define the logic in the referenced process to localise the impact when the logic changes in the future.

Design rEsTful API design in the specification stage assuming microservices

REST is widely used as a protocol for inter-service communication in microservices. We will design RESTful APIs for HTTP request methods and URIs for each process, and think their meanings of HTTP response status codes sufficiently at the specification stage. This will be useful for analyzing the data obtained by monitoring the production environment. For example, if the precondition of a process is evaluated to false with the values of input variables, we can design to return “412 Precondition Failed”, which is one of the client errors.

Quality improvement through formal specification testing and the use of test cases in program testing

Formal specification testing is a dynamic analysis of a specification, which aims to confirm the satisfiability and validity of the specification, and to verify that the refinement process has been carried out correctly [5]. If we can show that the specification is satisfiable, we can say that there exists a model (program) that satisfies the specification.

Program testing is done by putting values into input variables for the program and comparing the calculated output variable values with the expected output variable values. Formal specification testing, on the other hand, involves entering values for both input and output variables for a formal specification, and analyzing and comparing the truth values of the pre- and post-conditions that emerge from evaluating the specification. Figure 6 shows the criteria when we perform Formal Specification Testing for Satisfiability.

Figure 6. Formal specification testing.

By conducting formal specification testing, QA engineers can gain a better understanding of the specification itself and, in some cases, can improve the specification through further interaction with users. In addition, the input and output values used in the formal specification testing can be used for program testing.

Version control of both formal specification and implementation

In DevOps, continuous integration is practiced by automating the build and testing of program source code using version control tools such as Git repositories.

In formal specifications, we also use version control tools to manage changes, which leads to improved maintainability.

Management of libraries used in implementation at the specification stage

In microservices, it is desirable to cooperate with other services using HTTP-based REST or messaging, but there are cases where specific product libraries are used for access. In the mid-to-long term, such a library may need to be changed to a new version and you may need to change the program to fit the new library, for example in case the authentication method is updated. The problem that arises here is the impact of the change in the library.

Therefore, QA engineers record the libraries used by developers and their versions against the specifications through dialogues with developers. If there is a change in the library, the scope of the impact can be investigated and understood based on the specification.

Changes from the formal specification

Whenever you need to make changes to a program, start with a formal specification. By examining the formal specification, it is possible to understand the impact of the change. If the specification itself needs to be changed as a result, always start with the formal specification. Observe the order of change and evolution to prevent inconsistencies between the specification and the implementation.

Continuous monitoring

In DevOps, monitoring in operation is important to ensure continuous quality. When evolving a program, we run the service before and after the evolution in a blue-green deployment in a real environment to check for unexpected delays and HTTP response status codes. At that time, we will refer to the RESTful API design implemented in the specification phase for data analysis.

Responding to evolution

In this chapter, we will take some examples of evolution, describe how DevFemOps can address them, and identify the benefits of DevFemOps for evolution.

Evolution of some microservices

When evolving a certain microservice, we analyse the CDFD of SOFL to understand the impact of the change.

For example, when the upper process P2 in Figure 7 evolves into the lower process P2’, we can focus on the input IP2 and output OP2 in the process P2, and if the evolution has no impact on both input and output, we can localise the impact to only one service (e.g. P2 in Figure 7). In the case of an evolution that affects the input IP2 (IP2’), it is necessary to consider the impact on the process P1 that is related to IP2. Similarly, in the case of an evolution that affects the output OP2 (OP2’), process P3 should be considered.

Figure 7. CDFD analysis for evolution.

In DevFemOps, the relationships between microservices are expressed in CDFD, which can be used to analyse the scope of influence in evolution.

Changing technology trends

One of the characteristics of microservices is that each service is developed autonomously by each team. The services are loosely coupled by using HTTP-based REST and messaging. Therefore, each service can be implemented in a different programming language.

When we need to make some changes to a service, it may be more cost effective in some cases to radically rebuild the service. From a medium- to long-term perspective, changes in technology trends may lead to the emergence of programming languages that are better than those used in the current service and that have a higher level of maturity in the team.

In the case of DevFemOps, there is a formal specification for each service and a formal specification for the relationship between services. Developers do not need to figure out user requirements from existing program code that describes how to achieve them, but can autonomously implement services in any programming language from formal specifications that describe what the user requirements are.

Business changes

In this section, we call business change that a service changes due to some external factors. For example, from a mid-to-long term perspective, a microservice may be calling an API for some service, and the authentication method may change. If you are using a library to make API calls, you may need to upgrade to a library that supports the new authentication method. In this case, we want to understand how much of an impact updating the library will have.

Since DevFemOps manages the libraries used in the implementation at the specification stage, it is possible to determine which microservices will be affected by changes in a certain library by examining the specification.

Changing user requirements

When a service is operated over a medium to long period of time, new user requirements may emerge. In microservices, new services can be added without affecting the existing services.

In DevFemOps, the design of a new service starts from the formal specification and is implemented based on that specification, thus maintaining consistency between the formal specification and the implementation.

Maintainability and DevFemOps

In this section, we discuss how much DevFemOps can contribute to maintainability.

In engineering, maintainability is the ease with which a product can be maintained in order to the follows (Wikipedia, 2021):

1. Correct defects or their cause.

2. Repair or replace faulty or worn-out components without having to replace still working parts.

3. Prevent unexpected working conditions.

4. Maximise a product's useful life.

5. Maximise efficiency, reliability, and safety.

6. Meet new requirements.

7. Make future maintenance easier.

8. Cope with a changing environment.

Figure 8 shows the relationship of DevFemOps features to each of the above and maintainability objectives.

Figure 8. Relationship between maintainability and DevFemOps.

Figure 8 shows that there are some features of DevFemOps that satisfy each of the maintainability objectives, and that DevFemOps can contribute to ease of maintenance.

Conclusion

In this paper, we proposed DevFemOps as a way to increase maintainability and achieve continuous quality improvement. We also defined the DevFemOps QA engineer as a new role within the agile development squad that is responsible for the quality of the product, and described how the DevOps cycle, with the QA engineer at the center, can bring us closer to the goal we are aiming for with DevFemOps. In addition, we discussed how the features of DevFemOps can contribute to ease of maintenance.

We will conduct a systematic experiment in our future research. Then, we would like to apply DevFemOps to actual projects, verify its effectiveness, and refine the role that DevFemOps QA engineers should have. We also would like to create a tool to support DevFemOps.

Acknowledgment

This research was supported by ROIS NII Open Collaborative Research 2021-(21FS02).

Disclosure statement

No potential conflict of interest was reported by the author(s).

Additional information

Funding

This work was supported by ROIS NII Open Collaborative Research: [Grant Number 2021-(21FS02)].

Notes on contributors

Tetsuo Fukuzaki

Tetsuo Fukuzaki is a doctoral student at Hiroshima University, Japan. He holds a B.Sc. and a M.Sc. degree in Information Engineering from Hiroshima City University, Japan. He has been working for IBM Japan since April 2000 as an IT Engineer. His research interests include formal engineering methods, cloud computing and software maintenance.

Shaoying Liu

Shaoying Liu is a Professor in Software Engineering at Hiroshima University. His research interests include formal engineering methods, software testing, human-machine pair programming, and intelligent software engineering environments. He has published 1 book, 12 edited books, and more than 250 papers in journals and conferences. He is IEEE Fellow and BCS Fellow.

Michael Butler

Michael Butler is Dean of the Faculty of Engineering and Physical Sciences and a Professor of Computer Science. His research is in the area of mathematical methods for design and verification of safe and secure software-based systems. He holds a B.A.(Hons) degree in Computer Science from Trinity College Dublin, Ireland, and a M.Sc. and D.Phil. degree in Computation from University of Oxford.