Prologue

   

본 교재는 저자가 대학원 연구원과 함께 7년 동안 개발한 SAVE 정형기법 도구에 관한 것이다.

 

도구의 필요성은 아무리 강조해도 부족하지 않다. 하지만, 과학과 공학을 전공하는 전문가의 입장에서는, 전문가가 고안한 이론을 입증하기 위한 수단으로서의 도구는 절대적일 수밖에 없다. 과거 본인의 박사논문의 재·역공학이론을 입증하기 위해 개발한 SRE (Software Re/reverse-engineering Environment) 도구도, 5명 이상의 전문가가 5년 이상을 걸려 개발한 관련 도구를 기반으로 본인이 같은 동료와 함께 4년 이상의 시간을 들여 확장한 SW 재·역공학 도구였다. 즉 전문가 5명이 거의 10년 가까이 개발한 도구였다. 그것도 DECDesign이라는 Meta-CASE 도구를 사용했음에도 불구하고.

 

이러한 장기간의 고난도 문제를 해결하기 위한 방법으로, 각 도메인에 적합한 Meta-Modeling 도구를 활용하는 것이 현재 시스템과 SW 공학의 대세다. 이러한 관점에서, 본 도서는 ADOxx Meta-Modeling Platform을 기반으로, SW 순공학 (Forward Engineering) 중, 시스템과 SW의 설계과정에서 요구되는, dTP-Calculus와 GTS logic과 같은 정형기법을 위한 SAVE (Specification, Analysis, Verification, Evaluation) 도구의 개발이 어떻게 구현되었는가에 대한 방법을 다루고 있다. 이러한 구현 방법은, 초기 전문가 3~5명이 10여년의 시간이 걸릴 것이라고 예상되었던, 관련 정형기법 도구의 개발 기간을 급격히 줄게 하였을 뿐만 아니라, 관련 도구의 기능이 도메인 관점에서 전문적으로 정형화될 수 있게 하였다. 그 결과, 초기 이동성을 위한 d-Calculus에 기반한 SAVE 1.0을 개발하는 기간은 거의 1년 정도가 소요되었고, 이후, 시간을 위한 dT-Calculus에 기반한 SAVE 2.0을 개발하는 기간은 거의 2년, 확률을 위한 dTP-Calculus에 기반한 SAVE 3.0을 개발하는 기간도 거의 2년 정도가 소요되었다. 그리고 현재는 AI를 위한 SAVE 4.0을 개발하고 있다.

 

SAVE 정형기법 도구 개발과정에서 우리는 필연적으로 해결해야 할 과제에 직면하게 되었다. 그것은 바로 개발 방법론에 관한 문서화였다. 왜냐하면, 도구 개발 방법론이 문서화되지 않는다면, 우리의 정형기법 도구 개발 방법론은 극히 비공학적일 수 밖에 없다는 모순에 빠지기 때문이었다.

 

이러한 모순과 더불어, 현장에서 요구되는 문서화는 직접적이며 현실적이었다. 저자들은 최근까지 SAVE에 기반한 dTP-Calculus와 GTS Logic에 관한 연구를 꾸준히 학회에 발표해 왔었다. 하지만, 이 과정에서 SAVE 도구 자체에 대한 연구와 결과를 학회에 발표하는 데는 학술적인 한계가 있었다. 또한 SW 공학 관련 정형기법에 대한 대학원과 학부 수업에서, SW 개발자의 입장에서 필수적인, 도구 개발을 위한 교육과 실기에 필요한 교재가 거의 부재함을 알게 되었다. 이러한 이유가 바로, SAVE 도구를 개발하던 연구원들과 같이 본 교재를 저술하게 된 동기였다.

 

본 교재의 개발은 2020년 봄부터 이성현 연구원과 송준섭 연구원과 같이 기획한 OMiLAB KOREA 연구소의 도전 과제였다. 코로나 위기에 따른, 격동의 가상 연구 환경에서 최종 결과가 나오기까지 다소 시간이 걸리긴 하였지만, 그래도, 이렇게 연구원이 과제의 책임자가 되어, 교재를 출판할 수 있게 된 것은 대단한 결과임에 분명하다. 또한, 지원되는 연구비가 없는 상황에서, 이성현 연구원과 송준섭 연구원이, 자발적으로, 이러한 도전에 동참한 것은, 부족한 지도교수로서, 대단한 결과 이상의 진정한 고마움을 느낀다. 늦게나마, 이성현 연구원과 송준섭 연구원에게, “이 세상에는 절대 돈으로 살 수 없는 것이 있다” 라는 학자의 명예를 같이 누릴 수 있는, 노년의 지도교수로서, “명예로운 도전의 조그만 결실이, 진정, 가치있다” 라는, 진심 어린 칭찬을, 소중한 제자에게, 전하고 싶다.

 

우리 대한민국의 현실은 SCI/E 논문이라는 지표에 눈이 멀어, 도구의 필요성을 외면한 지가 어언 25년이 넘어간다. 도구가 필요하면, “구매해서 쓰면 된다”고 하였던 25년 전의 정책은, 지금도 지속되고 있다. 이 결과, 대한민국은 도구를 개발할 수 있는 전문 인력이 고갈되었고, 도구는 외제품으로 난무해졌다. Smart Phone을 개발하기 위한, 많은 장비가 외제인 것처럼, 국내의 SW를 개발하는 많은 도구가 외제이다. 하지만, 우리의 HW를 개발하기 위한 장비의 국산화가 절대적일 수밖에 없는 것처럼, 우리의 SW를 개발하기 위한 도구의 국산화도 절대적일 수밖에 없다. 그렇지 않을 경우, 우리의 HW와 SW 산업은 모래 위에 성을 쌓는 것과 같기 때문이다. 이러한 면에서, OMiLAB Global의 ADOxx Meta-Modeling Platform은 우리에게 부러움의 대상일 수밖에 없다. 그리고, 나아가, 이러한 Platform을 Open Platform으로 우리 모두가 공유할 수 있게 제공한, OMiLAB Global의 철학은 위대할 수밖에 없다. 이러한 면에서, 공유의 기회와 개발의 도전을 마련해 준, 오스트리아 비엔나대학교의 Karagiannis 교수님께 진심으로 감사의 말씀을 전한다.

 

 

2021년 12월 30일

전주全州 화산華山 앞에서

 

 

OMiLAB Korea 연구소장, 저자 이문근

 

 

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. It 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 25 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