{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T14:53:32Z","timestamp":1778338412636,"version":"3.51.4"},"reference-count":34,"publisher":"World Scientific Pub Co Pte Ltd","issue":"04","funder":[{"name":"ROIS NII Open Collaborative Research 2021","award":["21FS02"],"award-info":[{"award-number":["21FS02"]}]},{"DOI":"10.13039\/501100010890","name":"Chinese Government Scholarship","doi-asserted-by":"publisher","award":["CSC No. 202108050145"],"award-info":[{"award-number":["CSC No. 202108050145"]}],"id":[{"id":"10.13039\/501100010890","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2022,4]]},"abstract":"<jats:p> Formal specifications can provide a solid foundation for software development and support for techniques of software quality assurance, such as specification-based inspection and testing. To ensure that these techniques can be applied effectively in practice, efficiently and accurately understanding specifications becomes extremely important. While this may be relatively easy for well-trained developers in formal methods, it can be rather difficult for computer since computer does not easily understand specifications. This difficulty poses a challenge for realizing automatic specification-based verification techniques that are in high demand for reducing development cost and improving software reliability. In this paper, we address this problem by discussing how the formal specification can be transformed into a knowledge graph to provide comprehensible, well-organized details of the specification for developers and computers. The transformation is done by extracting and storing information about attributes of each component and by establishing relationships between components in a formal specification. We elaborate on a top-down approach of constructing a knowledge graph from a specification, including creating an ontology, designing the Entity\u2013Relationship (ER) diagram of the relational database based on the created ontology, extracting and storing attribute and relationship information in the relational database, mapping ontology to its instances and relational data to RDF triples, and displaying knowledge graph. Further, we present a case study to show how our approach works on the formal specification of an ATM system. Finally, we describe three experiments to evaluate its performance in improving specification readability, effectively guiding inspectors to establish traceability links between specifications and programs, and detecting defects through program inspection, respectively. <\/jats:p>","DOI":"10.1142\/s0218194022500279","type":"journal-article","created":{"date-parts":[[2022,4,12]],"date-time":"2022-04-12T16:52:52Z","timestamp":1649782372000},"page":"605-644","source":"Crossref","is-referenced-by-count":14,"title":["Knowledge Graph Construction for SOFL Formal Specifications"],"prefix":"10.1142","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2896-2282","authenticated-orcid":false,"given":"Jiandong","family":"Li","sequence":"first","affiliation":[{"name":"Graduate School of Advanced Science and Engineering, Hiroshima University, Hiroshima 739-8527, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6748-5052","authenticated-orcid":false,"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[{"name":"Graduate School of Advanced Science and Engineering, Hiroshima University, Hiroshima 739-8527, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ai","family":"Liu","sequence":"additional","affiliation":[{"name":"Graduate School of Advanced Science and Engineering, Hiroshima University, Hiroshima 739-8527, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Runhe","family":"Huang","sequence":"additional","affiliation":[{"name":"Faculty of Computer and Information Sciences, Hosei University, Tokyo 184-8584, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2022,5,13]]},"reference":[{"key":"S0218194022500279BIB001","volume-title":"Formal Engineering for Industrial Software Development Using the SOFL method","author":"Liu S.","year":"2013"},{"key":"S0218194022500279BIB002","doi-asserted-by":"publisher","DOI":"10.1109\/32.663996"},{"key":"S0218194022500279BIB003","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock J.","year":"1996"},{"key":"S0218194022500279BIB004","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"S0218194022500279BIB005","volume-title":"Industrial Applications of Formal Methods to Model, Design and Analyze Computer Systems: An International Survey","author":"Craigen D.","year":"1995"},{"key":"S0218194022500279BIB006","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.1998.706660"},{"issue":"5","key":"S0218194022500279BIB007","doi-asserted-by":"crossref","first-page":"1100","DOI":"10.1109\/TSE.2011.102","volume":"38","author":"Liu S.","year":"2012","journal-title":"IEEE Trans. Softw. Eng."},{"key":"S0218194022500279BIB008","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2999884"},{"key":"S0218194022500279BIB009","doi-asserted-by":"publisher","DOI":"10.1109\/QRS.2016.56"},{"key":"S0218194022500279BIB010","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2021.3078714"},{"key":"S0218194022500279BIB011","doi-asserted-by":"publisher","DOI":"10.1109\/QRS54544.2021.00094"},{"key":"S0218194022500279BIB012","doi-asserted-by":"publisher","DOI":"10.2200\/S01125ED1V01Y202109DSK022"},{"key":"S0218194022500279BIB013","doi-asserted-by":"publisher","DOI":"10.1016\/j.jnca.2021.103076"},{"key":"S0218194022500279BIB014","doi-asserted-by":"publisher","DOI":"10.1145\/3371158.3371202"},{"key":"S0218194022500279BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-15-4163-6_56"},{"key":"S0218194022500279BIB016","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-017-1718-y"},{"key":"S0218194022500279BIB017","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2019.8927285"},{"key":"S0218194022500279BIB018","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2019.8667969"},{"key":"S0218194022500279BIB022","doi-asserted-by":"publisher","DOI":"10.1109\/32.368133"},{"key":"S0218194022500279BIB023","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45654-6"},{"key":"S0218194022500279BIB024","doi-asserted-by":"publisher","DOI":"10.3233\/SW-170275"},{"key":"S0218194022500279BIB025","volume-title":"Proc. 19th Int. Unicode Conf.","author":"Martin J. D.","year":"2001"},{"key":"S0218194022500279BIB026","volume-title":"OWL 2 Web Ontology Language Conformance W3C Recommendation","author":"Smith M.","edition":"2"},{"issue":"4","key":"S0218194022500279BIB027","first-page":"4","volume":"1","author":"Musen M. A.","year":"2015","journal-title":"Assoc. Comput. Mach."},{"key":"S0218194022500279BIB031","doi-asserted-by":"publisher","DOI":"10.1006\/knac.1993.1008"},{"key":"S0218194022500279BIB032","first-page":"383","volume-title":"Proc. 2010 Conf. New Trends in Software Methodologies, Tools and Techniques","author":"Liu S.","year":"2010"},{"key":"S0218194022500279BIB033","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024651"},{"issue":"19","key":"S0218194022500279BIB035","first-page":"1869","volume":"118","author":"Zhao Z.","year":"2018","journal-title":"Int. J. Pure Appl. Math."},{"key":"S0218194022500279BIB036","first-page":"3","volume-title":"Proc. Int. Workshop on Structured Object-Oriented Formal Language and Method","author":"Liu S.","year":"2018"},{"key":"S0218194022500279BIB037","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2973928"},{"key":"S0218194022500279BIB038","doi-asserted-by":"publisher","DOI":"10.1145\/3241741"},{"key":"S0218194022500279BIB039","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2021.3070843"},{"key":"S0218194022500279BIB040","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380418"},{"key":"S0218194022500279BIB041","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-2239-5"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194022500279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,26]],"date-time":"2022-05-26T08:17:36Z","timestamp":1653553056000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218194022500279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4]]},"references-count":34,"journal-issue":{"issue":"04","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["10.1142\/S0218194022500279"],"URL":"https:\/\/doi.org\/10.1142\/s0218194022500279","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4]]}}}