Prologue

This textbook is about the SAVE formal method tool that I and the graduate researchers in the OMiLAB Korea Research Center have developed for 7 years.

It is not good enough how strongly the necessity of the tools is emphasized. However, in the perspective of scientists and engineers as professionals, it is an absolute condition or requirement for them that the tools are the most critical means to prove their theories or concepts.

In the past, it took over 4 years for me and my colleagues to develop the SRE (Software Re/reverse-engineering Environment) tool, as the practical means to prove the concepts of a SW re/reverse engineering methodology for my Ph.D. thesis, extended from the existing SRE tool which had been developed by other 5 professionals for 5 years before my extension. I means that 5 professionals spent about 10 years to develop the SRE tool, even though utilizing a META-CASE tool, called DECDesign.

In order to solve such an extensively-time-consuming tool development, now it is a trend to apply Domain-Specific Meta-Modeling tools which are applicable to each specific domains. In that perspective, this textbook deals with the method how a formal method tool, called SAVE (Specification, Analysis, Verification, Evaluation), for dTP-Calculus and GTS logic, which is required at the time of system or SW design activity during the forward engineering process, has been implemented, based on ADOxx Meta-Modeling Platform. Such an implementation method reduces the tool development time drastically, which had been expected to require more than 10 years with the 3~5 Ph.D.-level developers, and makes the formal method tools be more professionally developed in the domain perspective.

As a result, it took about 1 year to develop the first version of the tool, that is, the SAVE 1.0, to realize the early version of the primitive movement actions for d-Calculus; about 2 years to develop the next version of the tool, that is, the SAVE 2.0, to realize the early version of the primitive temporal properties for dT-Calculus; about 2 years to develop the next version of the tool, that is, the SAVE 3.0, to realize the early version of the probability properties for dTP-Calculus. Currently the SAVE 4.0 has been developing to realize the application of the dTP-Calculus for the AI applications, especially, for Smart IoT Systems.

During this process of developing the SAVE tool, we faced with a task that we had to solve definitely, that is, documentation for the development methodology. The reason was that we might fall into our own contradiction that our formal method tool development methodology could be totally out of the system or SW engineering process if our methodology itself was not properly documented in that perspective of the engineering process.

In addition to the problem, such documentations were directly required and requested from the experts in the real field in practice. However, we realized, during the development process, that there were academical limitations to solve the task and problems only by reporting the tool and its capabilities in the conferences and journals. In addition, we realized that there were no enough materials, such as textbooks and guidances, to be used in the lectures and exercises for formal methods in the undergraduate and graduate courses in the field of System and SW engineering. This is the reason why we published this textbook for the SAVE tool which we had worked on for years.

The publication of the textbook was a kind of a challenging task for OMiLAB Korea Reseach Center, pursued by the researchers in the center, that is, Sunghyun Lee and Junsup Song. Due to the COVID-19 crisis, it took more time and efforts than expected, especially in the virtual research environment, but it is definitely a great outcome that this textbook is finally published with respect to the fact that they played the role of leaders for the task at their graduate-level research positions. In addition, I, as an advisor, feel a sort of sincere gratitude to their voluntary participation to this challenging task of the publication without any financial supports. I know that it is too late, but I want to express myself to them, as my students, with my heartful praise, that “truly worthy is the humble outcome from the honorable challenges,”in the perspective of an old professor that “there is something that cannot be bought with money.”

It is our explicit reality in Korea that it has been more than 15 years since we ignored the importance of the capabilities to develop the tools, while focusing only on the SCI blindness in our academy and researches. Still continues the 25 years old policy that the tools can be “purchased for use” if they are needed. As a result, there are lack of professionals and engineers who can develop the tools, and the foreign tool from outside are full all over the place in every domains. As, in reality, the foreign instruments are needed to produce smart phone in Korea, the foreign tools, in reality, are needed to develop SW and systems in Korea, too. However, as it is our challenging critical task for us to produce the instruments domestically for the hardwares, it is also our challenging critical task for us to produce the tools domestically for the softwares. If not, the HW and SW industries in Korea would be like being built on the sand foundation. In that perspective, ADOxx Meta-Modeling Platform of OMiLAB Global could be one of our target tools that we have to learn from. And, in that perspective, truly great shall be the philosophy that the ADOxx platform can be shared with everyone in the world, as an open platform.

In that perspective, I express my true and sincere gratitude to Prof. Karagiannis in The University of Vienna who has provided me with this valuable opportunity and challenge in the future world of the openness.

30th December 2021

At the front of Hwa Mountain 

Head of OMiLAB Korea Research Center

Prof. Ph.D. Moonkun Lee