{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T06:38:03Z","timestamp":1768891083196,"version":"3.49.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"grants"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>In this article, we present ConceVE, an approach for designing and validating models before they are implemented in a computer simulation. The approach relies on (1) domain-specific languages for model specification, (2) the Alloy Specification Language and its constraint solving analysis capabilities for exploring the state space of the model dynamically, and (3) supporting visualization tools to relay the results of the analysis to the user. We show that our approach is applicable with generic languages such as the Web Ontology Language as well as special XML-based languages such as the Coalition Battle Management Language.<\/jats:p>","DOI":"10.1145\/2567897","type":"journal-article","created":{"date-parts":[[2014,4,1]],"date-time":"2014-04-01T13:06:54Z","timestamp":1396357614000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["ConceVE"],"prefix":"10.1145","volume":"24","author":[{"given":"Ross","family":"Gore","sequence":"first","affiliation":[{"name":"Old Dominion University, Suffolk, VA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saikou","family":"Diallo","sequence":"additional","affiliation":[{"name":"Old Dominion University, Suffolk, VA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose","family":"Padilla","sequence":"additional","affiliation":[{"name":"Old Dominion University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/379525.379526"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/288195.288251"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Grigoris Antoniou and Frank van Harmelen. 2009. Web ontology language: Owl. Handbook on Ontologies 91--110.  Grigoris Antoniou and Frank van Harmelen. 2009. Web ontology language: Owl. Handbook on Ontologies 91--110.","DOI":"10.1007\/978-3-540-92673-3_4"},{"key":"e_1_2_1_4_1","volume-title":"International Joint Conference on Artificial Intelligence","volume":"19","author":"Batt Gr\u00e9gory","year":"2005","unstructured":"Gr\u00e9gory Batt , Delphine Ropers , Hidde De Jong , Johannes Geiselmann , Radu Mateescu , Michel Page , Dominique Schneider , 2005 . Analysis and verification of qualitative models of genetic regulatory networks: A model-checking approach . In International Joint Conference on Artificial Intelligence , Vol. 19 . Lawrence Erlbaum Associates Ltd., 370. Gr\u00e9gory Batt, Delphine Ropers, Hidde De Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, Dominique Schneider, et al. 2005. Analysis and verification of qualitative models of genetic regulatory networks: A model-checking approach. In International Joint Conference on Artificial Intelligence, Vol. 19. Lawrence Erlbaum Associates Ltd., 370."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_13"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/229493.229511"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836090"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1993.0025"},{"key":"e_1_2_1_9_1","volume-title":"Morse","author":"Brutzman Don","year":"2002","unstructured":"Don Brutzman , Michael Zyda , J. Mark Pullen , and Katherine L . Morse . 2002 . Extensible Modeling and Simulation Framework (XMSF): Challenges for Web-Based Modeling and Simulation. Naval Postgraduate Schoo, Monterey, CA. Don Brutzman, Michael Zyda, J. Mark Pullen, and Katherine L. Morse. 2002. Extensible Modeling and Simulation Framework (XMSF): Challenges for Web-Based Modeling and Simulation. Naval Postgraduate Schoo, Monterey, CA."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 34th Conference on Winter Simulation: Exploring New Frontiers. Winter Simulation Conference, 606--615","author":"Chandrasekaran Senthilanand","unstructured":"Senthilanand Chandrasekaran , Gregory Silver , John A. Miller , Jorge Cardoso , and Amit P. Sheth . 2002. XML-based modeling and simulation: Web service technologies and their synergy with simulation . In Proceedings of the 34th Conference on Winter Simulation: Exploring New Frontiers. Winter Simulation Conference, 606--615 . Senthilanand Chandrasekaran, Gregory Silver, John A. Miller, Jorge Cardoso, and Amit P. Sheth. 2002. XML-based modeling and simulation: Web service technologies and their synergy with simulation. In Proceedings of the 34th Conference on Winter Simulation: Exploring New Frontiers. Winter Simulation Conference, 606--615."},{"key":"e_1_2_1_12_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2000","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 2000 . Model Checking. MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2000. Model Checking. MIT Press."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/829532.831357"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2005.07.007"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1177\/003754976600600306"},{"key":"e_1_2_1_16_1","volume-title":"Embedded System Design: Modeling, Synthesis and Verification","author":"Gajski Daniel D.","unstructured":"Daniel D. Gajski , Samar Abdi , Andreas Gerstlauer , and Gunar Schirner . 2009. Embedded System Design: Modeling, Synthesis and Verification . Springer . Daniel D. Gajski, Samar Abdi, Andreas Gerstlauer, and Gunar Schirner. 2009. Embedded System Design: Modeling, Synthesis and Verification. Springer."},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Christine Golbreich. 2004. Combining rule and ontology reasoners for the Semantic Web. Rules and Rule Markup Languages for the Semantic Web 6--22.  Christine Golbreich. 2004. Combining rule and ontology reasoners for the Semantic Web. Rules and Rule Markup Languages for the Semantic Web 6--22.","DOI":"10.1007\/978-3-540-30504-0_2"},{"key":"e_1_2_1_18_1","volume-title":"Owl to Alloy Documentation","author":"Gore Ross","year":"2012","unstructured":"Ross Gore , Saikou Diallo , and Jose Padilla . 2012a. Owl to Alloy Documentation . Old Dominion University , Suffolk, VA . VMASC- 2012 -09. Ross Gore, Saikou Diallo, and Jose Padilla. 2012a. Owl to Alloy Documentation. Old Dominion University, Suffolk, VA. VMASC-2012-09."},{"key":"e_1_2_1_20_1","volume-title":"Wing","author":"Guttag John V.","year":"1993","unstructured":"John V. Guttag , James J. Horning , Withs J. Garl , Kevin D. Jones , Andres Modet , and Jeannette M . Wing . 1993 . Larch : Languages and tools for formal specification. In Texts and Monographs in Computer Science. Citeseer . John V. Guttag, James J. Horning, Withs J. Garl, Kevin D. Jones, Andres Modet, and Jeannette M. Wing. 1993. Larch: Languages and tools for formal specification. In Texts and Monographs in Computer Science. Citeseer."},{"key":"e_1_2_1_21_1","first-page":"285","article-title":"Infinite automata and formal verification","volume":"2","author":"Harbola Aditya","year":"2012","unstructured":"Aditya Harbola , Deepti Negi , and Deepak Harbola . 2012 . Infinite automata and formal verification . International Journal of Advanced Research in Computer Science and Software Engineering 2 , 3, 285 -- 289 . Aditya Harbola, Deepti Negi, and Deepak Harbola. 2012. Infinite automata and formal verification. International Journal of Advanced Research in Computer Science and Software Engineering 2, 3, 285--289.","journal-title":"International Journal of Advanced Research in Computer Science and Software Engineering"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_24_1","volume-title":"OWLED","volume":"258","author":"Horridge Matthew","year":"2007","unstructured":"Matthew Horridge , Sean Bechhofer , and Olaf Noppens . 2007 . Igniting the OWL 1.1 Touch Paper: The OWL API . In OWLED , Vol. 258 . Citeseer, 6--7. Matthew Horridge, Sean Bechhofer, and Olaf Noppens. 2007. Igniting the OWL 1.1 Touch Paper: The OWL API. In OWLED, Vol. 258. Citeseer, 6--7."},{"key":"e_1_2_1_25_1","unstructured":"Daniel Jackson. 1999. A comparison of object modelling notations: Alloy uml and z. Unpublished Manuscript.  Daniel Jackson. 1999. A comparison of object modelling notations: Alloy uml and z. Unpublished Manuscript."},{"key":"e_1_2_1_26_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, Language, and Analysis . MIT Press . Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. MIT Press."},{"key":"e_1_2_1_27_1","volume-title":"Systematic Software Development Using VDM","author":"Jones Cliff B.","unstructured":"Cliff B. Jones . 1986. Systematic Software Development Using VDM , Vol. 66 . Prentice Hall . Cliff B. Jones. 1986. Systematic Software Development Using VDM, Vol. 66. Prentice Hall."},{"key":"e_1_2_1_28_1","unstructured":"Holger Knublauch. 2006. Protege-OWL API Programmers Guide.  Holger Knublauch. 2006. Protege-OWL API Programmers Guide."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266089"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176632"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1995456.1995462"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1995456.1995689"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1118890.1118892"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 37th Annual Simulation Symposium. IEEE, 55--63","author":"Miller John A.","unstructured":"John A. Miller , Gregory T. Baramidze , Amit P. Sheth , and Paul A. Fishwick . 2004. Investigating ontologies for simulation modeling . In Proceedings of the 37th Annual Simulation Symposium. IEEE, 55--63 . John A. Miller, Gregory T. Baramidze, Amit P. Sheth, and Paul A. Fishwick. 2004. Investigating ontologies for simulation modeling. In Proceedings of the 37th Annual Simulation Symposium. IEEE, 55--63."},{"key":"e_1_2_1_37_1","volume-title":"A Calculus of Communicating Systems","author":"Milner Robin","unstructured":"Robin Milner . 1982. A Calculus of Communicating Systems . Springer-Verlag , New York, NY . Robin Milner. 1982. A Calculus of Communicating Systems. Springer-Verlag, New York, NY."},{"key":"e_1_2_1_38_1","volume-title":"Ian Horrocks, Zhe Wu, Achille Fokoue, and Carsten Lutz.","author":"Motik Boris","year":"2009","unstructured":"Boris Motik , Bernardo Cuenca Grau , Ian Horrocks, Zhe Wu, Achille Fokoue, and Carsten Lutz. 2009 . Owl 2 web ontology language: Profiles. W3C Recommendation 27, 61. Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, Achille Fokoue, and Carsten Lutz. 2009. Owl 2 web ontology language: Profiles. W3C Recommendation 27, 61."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122012.1122013"},{"key":"e_1_2_1_40_1","first-page":"327","article-title":"Ideas about simulation conceptual model development","volume":"21","author":"Pace Dale K.","year":"2000","unstructured":"Dale K. Pace . 2000 . Ideas about simulation conceptual model development . Johns Hopkins APL Technical Digest 21 , 3, 327 -- 336 . Dale K. Pace. 2000. Ideas about simulation conceptual model development. Johns Hopkins APL Technical Digest 21, 3, 327--336.","journal-title":"Johns Hopkins APL Technical Digest"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/259207.259375"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789812776303_0012"},{"key":"e_1_2_1_43_1","volume-title":"Simulation: The Practice of Model Development and Use","author":"Robinson Stewart","year":"2004","unstructured":"Stewart Robinson . 2004 . Simulation: The Practice of Model Development and Use . Wiley . Stewart Robinson. 2004. Simulation: The Practice of Model Development and Use. Wiley."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1218112.1218259"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1162708.1162736"},{"key":"e_1_2_1_46_1","volume-title":"Ontoviz Tab: Visualizing Prot\u00e9g\u00e9 Ontologies.","author":"Sintek Michal","year":"2003","unstructured":"Michal Sintek . 2003 . Ontoviz Tab: Visualizing Prot\u00e9g\u00e9 Ontologies. Michal Sintek. 2003. Ontoviz Tab: Visualizing Prot\u00e9g\u00e9 Ontologies."},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the Winter Simulation Conference. IEEE, 8","author":"Spiegel Michael","unstructured":"Michael Spiegel , Paul F. Reynolds Jr ., and David C. Brogan . 2005. A case study of model context for simulation composability and reusability . In Proceedings of the Winter Simulation Conference. IEEE, 8 pp. Michael Spiegel, Paul F. Reynolds Jr., and David C. Brogan. 2005. A case study of model context for simulation composability and reusability. In Proceedings of the Winter Simulation Conference. IEEE, 8 pp."},{"key":"e_1_2_1_48_1","volume-title":"Understanding Z: A Specification Language and Its Formal Semantics","author":"Spivey J. Michael","unstructured":"J. Michael Spivey . 1988. Understanding Z: A Specification Language and Its Formal Semantics . Vol. 3 . Cambridge University Press . J. Michael Spivey. 1988. Understanding Z: A Specification Language and Its Formal Semantics. Vol. 3. Cambridge University Press."},{"key":"e_1_2_1_49_1","first-page":"1","article-title":"Formal methods for service composition","volume":"1","author":"Ter Beek Maurice H.","year":"2007","unstructured":"Maurice H. Ter Beek , Antonio Bucchiarone , and Stefania Gnesi . 2007 . Formal methods for service composition . Annals of Mathematics, Computing and Teleinformatics 1 , 5, 1 -- 10 . Maurice H. Ter Beek, Antonio Bucchiarone, and Stefania Gnesi. 2007. Formal methods for service composition. Annals of Mathematics, Computing and Teleinformatics 1, 5, 1--10.","journal-title":"Annals of Mathematics, Computing and Teleinformatics"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/290274.290303"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 2006 Fall Simulation Interoperability Workshop.","author":"Tolk Andreas","year":"2006","unstructured":"Andreas Tolk , Saikou Diallo , and Chuck Turnitsa . 2006 . Merging protocols, grammar, representation, and ontological approaches in support of C-BML . In Proceedings of the 2006 Fall Simulation Interoperability Workshop. Andreas Tolk, Saikou Diallo, and Chuck Turnitsa. 2006. Merging protocols, grammar, representation, and ontological approaches in support of C-BML. In Proceedings of the 2006 Fall Simulation Interoperability Workshop."},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the 2007 Fall Simulation Interoperability Workshop.","author":"Tolk Andreas","year":"2007","unstructured":"Andreas Tolk , Saikou Diallo , and Chuck Turnitsa . 2007 . A system view of C-BML . In Proceedings of the 2007 Fall Simulation Interoperability Workshop. Andreas Tolk, Saikou Diallo, and Chuck Turnitsa. 2007. A system view of C-BML. In Proceedings of the 2007 Fall Simulation Interoperability Workshop."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1057\/jos.2013.3"},{"key":"e_1_2_1_54_1","first-page":"1","article-title":"Pi calculus versus Petri nets: Let us eat humble pie rather than further inflate the Pi hype","volume":"3","author":"Van der Aalst Wil M. P.","year":"2005","unstructured":"Wil M. P. Van der Aalst . 2005 . Pi calculus versus Petri nets: Let us eat humble pie rather than further inflate the Pi hype . BPTrends 3 , 5, 1 -- 11 . Wil M. P. Van der Aalst. 2005. Pi calculus versus Petri nets: Let us eat humble pie rather than further inflate the Pi hype. BPTrends 3, 5, 1--11.","journal-title":"BPTrends"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/352029.352035"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88643-3_7"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2567897","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2567897","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:39Z","timestamp":1750232079000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2567897"}},"subtitle":["Conceptual modeling and formal validation for everyone"],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2567897"],"URL":"https:\/\/doi.org\/10.1145\/2567897","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"value":"1049-3301","type":"print"},{"value":"1558-1195","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2013-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}