{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T13:55:07Z","timestamp":1725803707744},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105567"},{"type":"electronic","value":"9783319105574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10557-4_15","type":"book-chapter","created":{"date-parts":[[2014,8,27]],"date-time":"2014-08-27T08:12:24Z","timestamp":1409127144000},"page":"119-129","source":"Crossref","is-referenced-by-count":10,"title":["Critical Systems Verification in MetaMORP(h)OSY"],"prefix":"10.1007","author":[{"given":"Rocco","family":"Aversa","sequence":"first","affiliation":[]},{"given":"Beniamino","family":"Di Martino","sequence":"additional","affiliation":[]},{"given":"Francesco","family":"Moscato","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Bureau, A.T.S.: Ao-2008-070: In-flight upset, 154 km west of learmonth, wa, 7 october 2008. In: Airbus A330-303. Tech. rep (October 2008)"},{"key":"15_CR2","unstructured":"Williams, M.: Toyota to recall prius hybrids over abs software. In: Computerworld (2010)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Charette, R.N.: This car runs on code. IEEE Spectrum 46 (2009)","DOI":"10.1109\/MSPEC.2009.5340234"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Feiler, P.H.: Model-based validation of safety-critical embedded systems. In: 2010 IEEE Aerospace Conference, pp. 1\u201310. IEEE (2010)","DOI":"10.1109\/AERO.2010.5446809"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Hutchinson, J., Rouncefield, M., Whittle, J.: Model-driven engineering practices in industry. In: 2011 33rd International Conference on Software Engineering (ICSE), pp. 633\u2013642 (May 2011)","DOI":"10.1145\/1985793.1985882"},{"key":"15_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/MGS-2010-0139","volume":"6","author":"Z. Guessoum","year":"2010","unstructured":"Guessoum, Z., Briot, J.P., Faci, N., Marin, O.: Towards reliable multi-agent systems: An adaptive replication mechanism. Multiagent Grid Syst.\u00a06, 1\u201324 (2010)","journal-title":"Multiagent Grid Syst."},{"key":"15_CR7","unstructured":"Kavi, K.M., Aborizka, M., Kung, D., Texas, N.: A framework for designing, modeling and analyzing agent based software systems. In: Proc. of 5th International Conference on Algorithms and Architectures for Parallel Processing, pp. 23\u201325 (2002)"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1023\/B:AGNT.0000019691.42633.07","volume":"9","author":"V.T. Silva Da","year":"2004","unstructured":"Da Silva, V.T., De Lucena, C.J.P.: From a conceptual framework for agents and objects to a multi-agent system modeling language. Autonomous Agents and Multi-Agent Systems\u00a09, 145\u2013189 (2004)","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Moscato, F., Aversa, R., Amato, A.: Describing cloud use case in metamorp(h)osy. In: IEEE Proc. of CISIS 2012 Conference, pp. 793\u2013798 (2012)","DOI":"10.1109\/CISIS.2012.143"},{"key":"15_CR10","unstructured":"PapyrusGroup: Papyrus uml, \n                    \n                      http:\/\/www.papyrusuml.org"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Franceschinis, G., Gribaudo, M., Iacono, M., Marrone, S., Moscato, F., Vittorini, V.: Interfaces and binding in component based development of formal models. In: IEEE Proc. of VALUETOOLS 2009 Conference, vol.\u00a044 (2009)","DOI":"10.4108\/ICST.VALUETOOLS2009.7677"},{"issue":"1","key":"15_CR12","first-page":"83","volume":"9","author":"F. Moscato","year":"2012","unstructured":"Moscato, F., Vittorini, V., Amato, F., Mazzeo, A., Mazzocca, N.: Solution workflows for model-based analysis of complex systems. IEEE T. Automation Science and Engineering\u00a09(1), 83\u201395 (2012)","journal-title":"IEEE T. Automation Science and Engineering"},{"key":"15_CR13","unstructured":"Moscato, F., Martino, B.D., Aversa, R.: Enabling model driven engineering of cloud services by using mosaic ontology. Scalable Computing: Practice and Experience 13(1) (2012)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-70657-7_7","volume-title":"Agent-Oriented Software Engineering II","author":"B. Bauer","year":"2002","unstructured":"Bauer, B.: UML class diagrams revisited in the context of agent-based systems. In: Wooldridge, M.J., Wei\u00df, G., Ciancarini, P. (eds.) AOSE 2001. LNCS, vol.\u00a02222, pp. 101\u2013118. Springer, Heidelberg (2002)"},{"key":"15_CR15","first-page":"91","volume":"11","author":"B. Bauer","year":"2000","unstructured":"Bauer, B., M\u00fcller, J.P., Odell, J.: Agent uml: A formalism for specifying multiagent software systems. Int. Journal of Software Engineering and Knowledge Engineering\u00a011, 91\u2013103 (2000)","journal-title":"Int. Journal of Software Engineering and Knowledge Engineering"},{"key":"15_CR16","first-page":"391","volume":"29","author":"I. Trencansky","year":"2005","unstructured":"Trencansky, I., Cervenka, R.: Agent modeling language (aml): A comprehensive approach to modeling mas. Whitestein Series in Software Agent Technologies and Autonomic Computing\u00a029, 391\u2013400 (2005)","journal-title":"Whitestein Series in Software Agent Technologies and Autonomic Computing"},{"issue":"1","key":"15_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.engappai.2011.08.008","volume":"25","author":"J.M. Gascue\u00f1a","year":"2012","unstructured":"Gascue\u00f1a, J.M., Navarro, E., Fern\u00e1ndez-Caballero, A.: Model-driven engineering techniques for the development of multi-agent systems. Engineering Applications of Artificial Intelligence\u00a025(1), 159\u2013173 (2012)","journal-title":"Engineering Applications of Artificial Intelligence"},{"key":"15_CR18","series-title":"CCIS","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-11819-7_17","volume-title":"Agents and Artificial Intelligence","author":"A. Fern\u00e1ndez-Caballero","year":"2010","unstructured":"Fern\u00e1ndez-Caballero, A., Gascue\u00f1a, J.M.: Developing multi-agent systems through integrating prometheus, INGENIAS and ICARO-T. In: Filipe, J., Fred, A., Sharp, B. (eds.) ICAART 2009. CCIS, vol.\u00a067, pp. 219\u2013232. Springer, Heidelberg (2010)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11925040_8","volume-title":"Leveraging Applications of Formal Methods","author":"P.A. Abdulla","year":"2006","unstructured":"Abdulla, P.A., Deneux, J., St\u00e5lmarck, G., \u00c5gren, H., \u00c5kerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol.\u00a04313, pp. 115\u2013129. Springer, Heidelberg (2006)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Farines, J., De Queiroz, M., da Rocha, V., Carpes, A., Vernadat, F., Cregut, X.: A model-driven engineering approach to formal verification of plc programs. In: 2011 IEEE 16th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1\u20138 (September 2011)","DOI":"10.1109\/ETFA.2011.6058983"},{"key":"15_CR21","unstructured":"Moscato, F., Aversa, R., Martino, B.D., Fortis, T.F., Munteanu, V.I.: An analysis of mosaic ontology for cloud resources annotation. In: IEEE Proc. of FedCSIS 2011 Conference, pp. 973\u2013980 (2011)"},{"key":"15_CR22","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.trc.2014.02.002","volume":"42","author":"M. Ghazel","year":"2014","unstructured":"Ghazel, M.: Formalizing a subset of ertms\/etcs specifications for verification purposes. Transportation Research Part C: Emerging Technologies\u00a042, 60\u201375 (2014)","journal-title":"Transportation Research Part C: Emerging Technologies"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-662-43652-3_10","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"R.B. Ayed","year":"2014","unstructured":"Ayed, R.B., Collart-Dutilleul, S., Bon, P., Idani, A., Ledru, Y.: B formal validation of ERTMS\/ETCS railway operating rules. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol.\u00a08477, pp. 124\u2013129. Springer, Heidelberg (2014)"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"James, P., Moller, F., Nguyen, H., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. International Journal on Software Tools for Technology Transfer, 1\u201327 (2014)","DOI":"10.1016\/j.scico.2014.04.005"},{"key":"15_CR25","series-title":"SCI","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-85257-5_19","volume-title":"Intelligent Distributed Computing, Systems and Applications","author":"F. Moscato","year":"2008","unstructured":"Moscato, F., Venticinque, S., Aversa, R., Di Martino, B.: Formal modeling and verification of real-time multi-agent systems: The REMM framework. In: Badica, C., Mangioni, G., Carchiolo, V., Burdescu, D. (eds.) Intelligent Distributed Computing, Systems and Applications. SCI, vol.\u00a0162, pp. 187\u2013196. Springer, Berlin (2008)"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Wooldridge, M.: Agent-based software engineering. In: IEE Proceedings on Software Engineering, pp. 26\u201337 (1997)","DOI":"10.1049\/ip-sen:19971026"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Amato, F., Casola, V., Mazzocca, N., Romano, S.: A semantic-based document processing framework: a security perspective. In: 2011 International Conference on Complex, Intelligent and Software Intensive Systems (CISIS), pp. 197\u2013202. IEEE (2011)","DOI":"10.1109\/CISIS.2011.37"},{"issue":"4","key":"15_CR28","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1093\/jigpal\/jzs027","volume":"21","author":"F. Amato","year":"2013","unstructured":"Amato, F., Casola, V., Mazzocca, N., Romano, S.: A semantic approach for fine-grain access control of e-health documents. Logic Journal of IGPL\u00a021(4), 692\u2013701 (2013)","journal-title":"Logic Journal of IGPL"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Amato, F., Casola, V., Mazzeo, A., Romano, S.: A semantic based methodology to classify and protect sensitive data in medical records. In: 2010 Sixth International Conference on Information Assurance and Security (IAS), pp. 240\u2013246. IEEE (2010)","DOI":"10.1109\/ISIAS.2010.5604071"},{"key":"#cr-split#-15_CR30.1","doi-asserted-by":"crossref","unstructured":"Mens, T., Gorp, P.V.: A taxonomy of model transformation. Electronic Notes in Theoretical Computer Science\u00a0152, 125-142 (2006)","DOI":"10.1016\/j.entcs.2005.10.021"},{"key":"#cr-split#-15_CR30.2","unstructured":"Proceedings of the International Workshop on Graph and Model Transformation (GraMoT 2005) (2005)"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Bloomfield, R.: Fundamentals of european rail traffic management system-ertms. IET Standards (2006)","DOI":"10.1049\/ic.2006.0684"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Ciccozzi, F., Sjodin, M.: Enhancing the generation of correct-by-construction code from design models for complex embedded systems. In: 2012 IEEE 17th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1\u20134 (September 2012)","DOI":"10.1109\/ETFA.2012.6489716"},{"key":"15_CR33","unstructured":"Altera: Quartus ii, \n                    \n                      http:\/\/www.altera.com\/products\/software\/quartus-ii\/about\/qts-performance-productivity.html"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/3-540-46429-8_28","volume-title":"Computer Performance Evaluation. Modelling Techniques and Tools","author":"C. Hirel","year":"2000","unstructured":"Hirel, C., Sahner, R., Zang, X., Trivedi, K.S.: Reliability and performability modeling using SHARPE 2000. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol.\u00a01786, pp. 345\u2013349. Springer, Heidelberg (2000)"},{"key":"15_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-30578-1_3","volume-title":"Agent-Oriented Software Engineering V","author":"R. \u010cervenka","year":"2005","unstructured":"\u010cervenka, R., Tren\u010dansk\u00fd, I., Calisti, M., Greenwood, D.P.A.: AML: Agent modeling language toward industry-grade agent-based modeling. In: Odell, J.J., Giorgini, P., M\u00fcller, J.P. (eds.) AOSE 2004. LNCS, vol.\u00a03382, pp. 31\u201346. Springer, Heidelberg (2005)"},{"issue":"1","key":"15_CR36","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/TDSC.2004.11","volume":"1","author":"D. Nicol","year":"2004","unstructured":"Nicol, D., Sanders, W., Trivedi, K.: Model-based evaluation: from dependability to security. IEEE Transactions on Dependable and Secure Computing\u00a01(1), 48\u201365 (2004)","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"issue":"5","key":"15_CR37","doi-asserted-by":"publisher","first-page":"836","DOI":"10.1016\/j.infsof.2012.11.009","volume":"55","author":"R.K. Panesar-Walawege","year":"2013","unstructured":"Panesar-Walawege, R.K., Sabetzadeh, M., Briand, L.: Supporting the verification of compliance to safety standards via model-driven engineering: Approach, tool-support and empirical validation. Information and Software Technology\u00a055(5), 836\u2013864 (2013)","journal-title":"Information and Software Technology"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10557-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T14:01:53Z","timestamp":1558965713000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10557-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319105567","9783319105574"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10557-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}