{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T15:16:41Z","timestamp":1726413401358},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T00:00:00Z","timestamp":1578528000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T00:00:00Z","timestamp":1578528000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int. J. Inf. Secur."],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10207-019-00483-6","type":"journal-article","created":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T02:12:42Z","timestamp":1578535962000},"page":"695-710","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A language and a pattern system for temporal property specification: advanced metering infrastructure case study"],"prefix":"10.1007","volume":"19","author":[{"given":"Tina","family":"Tavizi","sequence":"first","affiliation":[]},{"given":"Mehdi","family":"Shajari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,1,9]]},"reference":[{"key":"483_CR1","unstructured":"Object Management Group: Unified Modeling Language (UML) Specification. Version 2.5 (2015). OMG document formal\/01 March 2015 [Online]. https:\/\/www.omg.org\/spec\/UML\/2.5.1"},{"key":"483_CR2","unstructured":"Object Management Group: Object Constraint Language (OCL) Specification. Version 2.4 (2014). OMG document formal\/03 February 2014 [Online]. https:\/\/www.omg.org\/spec\/OCL\/2.4\/"},{"key":"483_CR3","volume-title":"Modeling embedded systems and SoC\u2019s: concurrency and time in models of computation","author":"A Jantsch","year":"2004","unstructured":"Jantsch, A.: Modeling embedded systems and SoC\u2019s: concurrency and time in models of computation. Morgan Kaufmann, Burlington (2004)"},{"issue":"12","key":"483_CR4","doi-asserted-by":"publisher","first-page":"1217","DOI":"10.1109\/43.736561","volume":"17","author":"EA Lee","year":"1998","unstructured":"Lee, E.A., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 17(12), 1217\u20131229 (1998)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"483_CR5","first-page":"1","volume-title":"Models of Computation for Distributed Embedded Systems","author":"A Jantsch","year":"2009","unstructured":"Jantsch, A.: Models of Computation for Distributed Embedded Systems, pp. 1\u20133. CRC Press, Boca Raton (2009)"},{"issue":"2","key":"483_CR6","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/1667062.1667063","volume":"42","author":"CA Furia","year":"2010","unstructured":"Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling time in computing: a taxonomy and a comparative survey. ACM Comput. Surv. 42(2), 6 (2010)","journal-title":"ACM Comput. Surv."},{"key":"483_CR7","unstructured":"Object Management Group: UML Profile for MARTE Specification. Version 1.2 (2019). OMG document formal\/01 April 2019 [Online]. https:\/\/www.omg.org\/spec\/MARTE\/1.2\/"},{"key":"483_CR8","doi-asserted-by":"crossref","unstructured":"Latif, K.A., Rauf, A., Nadeem, A.: Evaluation of UML-real time profiles for industrial control systems. In: International Conference on Information and Emerging Technologies (ICIET), pp. 1\u20135 (2010)","DOI":"10.1109\/ICIET.2010.5625673"},{"key":"483_CR9","doi-asserted-by":"crossref","unstructured":"Zhang, M., Mallet, F.: An executable semantics of clock constraint specification language and its applications. In: International Workshop on Formal Techniques for Safety-Critical Systems, pp. 37\u201351. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-29510-7_2"},{"key":"483_CR10","unstructured":"Andr\u00e9, C.: Syntax and semantics of the clock constraint specification language (CCSL). Ph.D. diss., INRIA (2009)"},{"key":"483_CR11","unstructured":"Deantoni, J., Andr\u00e9, C., Gascon, R.: CCSL denotational semantics. Ph.D. diss., Array (2014)"},{"key":"483_CR12","unstructured":"Mallet, F., Millo, J.-V., Romenska, Y.: State-based representation of CCSL operators. Ph.D. diss., INRIA (2013)"},{"key":"483_CR13","unstructured":"Mallet, F.: UML profile for MARTE: time model and CCSL. In: ICTERI, pp. 289\u2013294 (2013)"},{"key":"483_CR14","unstructured":"Deantoni, J., Mallet, F.: ECL: the event constraint language, an extension of OCL with events. Ph.D. diss., INRIA (2012)"},{"key":"483_CR15","doi-asserted-by":"crossref","unstructured":"Kanso, B., Taha, S.: Temporal constraint support for OCL. In: International Conference on Software Language Engineering, pp. 83\u2013103. Springer Berlin Heidelberg (2012)","DOI":"10.1007\/978-3-642-36089-3_6"},{"key":"483_CR16","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Programming, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"483_CR17","doi-asserted-by":"crossref","unstructured":"Dou, W., Bianculli, D., Briand, L.: OCLR: a more expressive, pattern-based temporal extension of OCL. In: European Conference on Modelling Foundations and Applications, pp. 51\u201366. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-09195-2_4"},{"key":"483_CR18","unstructured":"Konrad, S., Cheng, B.H.: Real-time specification patterns. In: 27th International Conference on Software Engineering, 2005. ICSE 2005. Proceedings (pp. 372\u2013381). IEEE (2005)"},{"key":"483_CR19","unstructured":"Konrad, S., Cheng, B.H.C.: Defining and using real-time specification patterns for embedded systems. Technical Report of Michigan State University, MSUCSE-04-37, Revision of March 2006 (2006)"},{"issue":"2","key":"483_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.entcs.2005.10.035","volume":"153","author":"V Gruhn","year":"2006","unstructured":"Gruhn, V., Laue, R.: Patterns for timed property specifications. Electron. Notes Theor. Comput. Sci. 153(2), 117\u2013133 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"483_CR21","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jss.2008.06.041","volume":"82","author":"P Bellini","year":"2009","unstructured":"Bellini, P., Nesi, P., Rogai, D.: Expressing and organizing real-time specification patterns via temporal logics. J. Syst. Softw. 82(2), 183\u2013196 (2009)","journal-title":"J. Syst. Softw."},{"key":"483_CR22","doi-asserted-by":"crossref","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: ACM\/IEEE 30th International Conference on Software Engineering, 2008. ICSE\u201908, pp. 31\u201340. IEEE (2008)","DOI":"10.1145\/1368088.1368094"},{"key":"483_CR23","unstructured":"Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: 18th Annual IEEE Symposium on Logic in Computer Science, 2003. Proceedings, pp. 351\u2013360. IEEE (2003)"},{"issue":"7","key":"483_CR24","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1109\/TSE.2015.2398877","volume":"41","author":"M Autili","year":"2015","unstructured":"Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar. IEEE Trans. Softw. Eng. 41(7), 620\u2013638 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"483_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4129-7","volume-title":"Mathematical Logic for Computer Science","author":"M Ben-Ari","year":"2012","unstructured":"Ben-Ari, M.: Mathematical Logic for Computer Science. Springer, Berlin (2012)"},{"issue":"1","key":"483_CR26","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/349194.349197","volume":"32","author":"P Bellini","year":"2000","unstructured":"Bellini, P., Mattolini, R., Nesi, P.: Temporal logics for real-time system specification. ACM Comput. Surv. 32(1), 12\u201342 (2000)","journal-title":"ACM Comput. Surv."},{"key":"483_CR27","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Workshop\/School\/Symposium of the REX Project (Research and Education in Concurrent Systems), pp. 74\u2013106. Springer, Berlin (1991)","DOI":"10.1007\/BFb0031988"},{"key":"483_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"483_CR29","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logic of Programs, pp. 52\u201371. Springer, Berlin (1981)","DOI":"10.1007\/BFb0025774"},{"key":"483_CR30","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Safety metric temporal logic is fully decidable. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 411\u2013425. Springer, Berlin (2006)","DOI":"10.1007\/11691372_27"},{"key":"483_CR31","unstructured":"Hunter, P., Ouaknine, J., Worrell, J.: When is metric temporal logic expressively complete? arXiv preprint arXiv:1209.0516 (2012)"},{"key":"483_CR32","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.entcs.2009.02.044","volume":"231","author":"P Bouyer","year":"2009","unstructured":"Bouyer, P.: Model-checking timed temporal logics. Electron. Notes Theor. Comput. Sci. 231, 323\u2013341 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"483_CR33","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"6","key":"483_CR34","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"483_CR35","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1109\/32.910858","volume":"27","author":"R Mattolini","year":"2001","unstructured":"Mattolini, R., Nesi, P.: An interval logic for real-time system specification. IEEE Trans. Softw. Eng. 27(3), 208\u2013227 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"483_CR36","unstructured":"Moszkowski, B.C.: Reasoning about digital circuits. No. STAN-CS-83-970. Department of Computer Science, Stanford University, CA (1983)"},{"key":"483_CR37","doi-asserted-by":"crossref","unstructured":"Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: International Colloquium on Automata. Languages, and Programming, pp. 278\u2013291. Springer, Berlin (1983)","DOI":"10.1007\/BFb0036915"},{"key":"483_CR38","doi-asserted-by":"crossref","unstructured":"Greer, C., Wollman, D.A., Prochaska, D.E., Boynton, P.A., Mazer, J.A., Nguyen, C.T., FitzPatrick, G.J., Nelson, T.L., Koepke, G.H., Hefner, A.R., et al.: Nist framework and roadmap for smart grid interoperability standards release 3.0, US National Institute of Standards and Technology. Technical report (2014)","DOI":"10.6028\/NIST.SP.1108r3"},{"key":"483_CR39","unstructured":"The Advanced Security Acceleration Project, \u201cSecurity profile for advanced metering infrastructure,\u201d OpenSG Users Group (2009) [online]. http:\/\/osgug.ucaiug.org\/utilisec\/amisec\/Shared%20Documents\/AMI%20Security%20Profile%20(ASAP-SG)\/AMI%20Security%20Profile%20-%20v1_0.pdf"},{"key":"483_CR40","doi-asserted-by":"crossref","unstructured":"Nhlabatsi, A., Nuseibeh, B., Yu, Y.: Security requirements engineering for evolving software systems: a survey. In: Security-Aware Systems Applications and Software Development Methods, pp. 108\u2013128. IGI Global (2012)","DOI":"10.4018\/978-1-4666-1580-9.ch007"},{"issue":"1","key":"483_CR41","first-page":"64","volume":"11","author":"MRR Ramesh","year":"2016","unstructured":"Ramesh, M.R.R., Reddy, C.S.: A survey on security requirement elicitation methods: classification, merits and demerits. Int. J. Appl. Eng. Res. 11(1), 64\u201370 (2016)","journal-title":"Int. J. Appl. Eng. Res."},{"key":"483_CR42","doi-asserted-by":"crossref","unstructured":"Mu\u00f1ante, D., Chiprianov, V., Gallon, L., Aniort\u00e9, P.: A review of security requirements engineering methods with respect to risk analysis and model-driven engineering. In: International Conference on Availability. Reliability, and Security, pp. 79\u201393. Springer, Cham (2014)","DOI":"10.1007\/978-3-319-10975-6_6"},{"key":"483_CR43","unstructured":"Pub, F.I.P.S.: Standards for Security Categorization of Federal Information and Information Systems. NIST FIPS-199 (2004)"},{"key":"483_CR44","doi-asserted-by":"crossref","unstructured":"Deng, Y., Shukla, S.: A distributed real-time event correlation architecture for SCADA security. In: International Conference on Critical Infrastructure Protection, pp. 81\u201393. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-45330-4_6"},{"key":"483_CR45","unstructured":"SAE ARP4754A\/EUROCAE ED-79A, Guidelines for Development of Civil Aircraft and Systems, December 21 (2010)"},{"key":"483_CR46","unstructured":"SAE ARP 4761, Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems (1996)"},{"key":"483_CR47","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Pires, A.F., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S.: Formal design and safety analysis of AIR6110 wheel brake system. In: International Conference on Computer Aided Verification, pp. 518\u2013535. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_36"},{"key":"483_CR48","volume-title":"Safety Issues with Requirements Definition, Validation, and Verification Processes","author":"P De Salvo","year":"2014","unstructured":"De Salvo, P., Fogarty, D.: Safety Issues with Requirements Definition, Validation, and Verification Processes. Federal Aviation Administration, Aviation Research Division, Springfield (2014)"},{"key":"483_CR49","unstructured":"Berhens, H.: Specification, design and implementation of a flight control unit for an unmanned aerial vehicle. Ph.D. diss., Stellenbosch University, Stellenbosch (2015)"},{"key":"483_CR50","doi-asserted-by":"crossref","unstructured":"Tao, X., Zhu, Y., Mao, Y., Song, H., Liu, M., Liu, X., Sheng, W., Shi, W.: Designing ARINC653 partition constrained scheduling for secure real time embedded avionics. In: 2015 IEEE 2nd International Conference on Cyber Security and Cloud Computing, pp. 213\u2013217. IEEE (2015)","DOI":"10.1109\/CSCloud.2015.23"},{"key":"483_CR51","doi-asserted-by":"publisher","DOI":"10.1201\/b21425","volume-title":"Real-Time and Distributed Real-Time Systems: Theory and Applications","author":"A Gupta","year":"2016","unstructured":"Gupta, A., Chandra, A.K., Luksch, P.: Real-Time and Distributed Real-Time Systems: Theory and Applications. CRC Press, Boca Raton (2016)"},{"issue":"2s","key":"483_CR52","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/2465787.2465796","volume":"12","author":"FJ Cazorla","year":"2013","unstructured":"Cazorla, F.J., Qui\u00f1ones, E., Vardanega, T., Cucu, L., Triquet, B., Bernat, G., Berger, E., et al.: Proartis: probabilistically analyzable real-time systems. ACM Trans. Embed. Comput. Syst. 12(2s), 94 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst."}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-019-00483-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-019-00483-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-019-00483-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T19:53:33Z","timestamp":1610049213000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-019-00483-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,9]]},"references-count":52,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["483"],"URL":"https:\/\/doi.org\/10.1007\/s10207-019-00483-6","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"type":"print","value":"1615-5262"},{"type":"electronic","value":"1615-5270"}],"subject":[],"published":{"date-parts":[[2020,1,9]]},"assertion":[{"value":"9 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with ethical standards"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}