{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T15:10:06Z","timestamp":1751728206560,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319951645"},{"type":"electronic","value":"9783319951652"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-95165-2_17","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T14:35:04Z","timestamp":1530628504000},"page":"241-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Reasoning for Air Traffic Control System Using Event-B Method"],"prefix":"10.1007","author":[{"given":"Abdessamad","family":"Jarrar","sequence":"first","affiliation":[]},{"given":"Youssef","family":"Balouki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"issue":"1","key":"17_CR1","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0967-0661(93)92105-D","volume":"1","author":"NC Audsley","year":"1993","unstructured":"Audsley, N.C., Burns, A., Wellings, A.J.: Deadline monotonic scheduling theory and application. Control Eng. Pract. 1(1), 71\u201378 (1993)","journal-title":"Control Eng. Pract."},{"issue":"10","key":"17_CR2","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"3","key":"17_CR3","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/356698.356702","volume":"9","author":"JL Peterson","year":"1977","unstructured":"Peterson, J.L.: Petri nets, computing surveys. ACM Comput. Surv. 9(3), 223\u2013252 (1977)","journal-title":"ACM Comput. Surv."},{"issue":"1","key":"17_CR4","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14(1), 25\u201359 (1987)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"17_CR5","unstructured":"Spivey Oriel, J.M.: Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, New York, NY, USA \u00a9ISBN: 0-521-33429-2 (1988)"},{"issue":"11\u201312","key":"17_CR6","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1016\/j.scico.2009.07.006","volume":"74","author":"TS Hoang","year":"2009","unstructured":"Hoang, T.S., Kuruma, H., Basin, D., Abrial, J.R.: Developing topology discovery in Event-B. Sci. Comput. Program. 74(11\u201312), 879\u2013899 (2009)","journal-title":"Sci. Comput. Program."},{"key":"17_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"key":"17_CR8","unstructured":"Rodin, C., Jastram, M., Butler, M.: User\u2019s Handbook (2011)"},{"issue":"2","key":"17_CR9","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/j.ejor.2004.09.040","volume":"171","author":"H Pinol","year":"2006","unstructured":"Pinol, H., Beasley, J.E.: Scatter search and bionomic algorithms for the aircraft landing problem. Eur. J. Oper. Res. 171(2), 439\u2013462 (2006)","journal-title":"Eur. J. Oper. Res."},{"issue":"4","key":"17_CR10","doi-asserted-by":"publisher","first-page":"3485","DOI":"10.1016\/j.asoc.2011.01.022","volume":"11","author":"SP Yu","year":"2011","unstructured":"Yu, S.P., Cao, X.B., Zhang, J.: A real-time schedule method for aircraft landing scheduling problem based on cellular automation. Appl. Soft Comput. 11(4), 3485\u20133493 (2011)","journal-title":"Appl. Soft Comput."},{"key":"17_CR11","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-07512-9_2","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"W Su","year":"2014","unstructured":"Su, W., Abrial, J.-R.: Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 19\u201335. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_2"},{"issue":"1","key":"17_CR12","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/359970.359977","volume":"19","author":"NC Wilhelm","year":"1976","unstructured":"Wilhelm, N.C.: An anomaly in disk scheduling: a comparison of FCFS and SSTF seek scheduling using an empirical model for disk accesses. Commun. ACM 19(1), 13\u201317 (1976)","journal-title":"Commun. ACM"},{"issue":"3","key":"17_CR13","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1016\/0022-0000(92)90036-I","volume":"45","author":"U Schmid","year":"1992","unstructured":"Schmid, U., Blieberger, J.: Some investigations on FCFS scheduling in hard real time applications. J. Comput. Syst. Sci. 45(3), 493\u2013512 (1992)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"17_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/MMUL.2004.3","volume":"11","author":"J Jin","year":"2004","unstructured":"Jin, J., Nahrstedt, K.: QoS specification languages for distributed multimedia applications: a survey and taxonomy. IEEE Multimed. Mag. 11(3), 1\u201310 (2004)","journal-title":"IEEE Multimed. Mag."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Zafar, N.A.: Formal specification and analysis of take-off procedure using VDM-SL. Complex Adapt. Syst. Model. 5(5), (2016)","DOI":"10.1186\/s40294-016-0014-y"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Yousaf, S., Zafar, N.A., Khan, S.A.: Formal analysis of departure procedure of air traffic control system. In: 2010 2nd International Conference on Software Technology and Engineering (ICSTE), vol. 2 (2010)","DOI":"10.1109\/ICSTE.2010.5608802"},{"key":"17_CR17","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-319-07512-9_12","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"D M\u00e9ry","year":"2014","unstructured":"M\u00e9ry, D., Singh, N.K.: Modeling an aircraft landing system in Event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 154\u2013159. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_12"},{"key":"17_CR18","unstructured":"M\u00e9ry, D., Kumar Singh, N.: EB2J : Code generation from Event-B to Java. In: SBMF - Brazilian Symposium on Formal Methods, S\u00e3o Paulo, Brazil (2011)"},{"key":"17_CR19","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-64719-7_12","volume-title":"International Conference on Information Technology and Communication Systems","author":"A Jarrar","year":"2018","unstructured":"Jarrar, A., Balouki, Y., Gadi, T., Chougdali, S.: Modeling aircraft landing scheduling in Event B. In: Noreddine, G., Kacprzyk, J. (eds.) ITCS 2017. AISC, vol. 640, pp. 127\u2013142. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-64719-7_12"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Jarrar, A., Bellasri, O., Chougdali, S., Balouki, Y.: Formal specification and verification of transmission control protocol. In: Proceedings of the 2nd International Conference on Computing and Wireless Communication Systems, p. 30. ACM (2017)","DOI":"10.1145\/3167486.3167516"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Jarrar, A., Gadi, T., Balouki, Y.: Modeling the internet of things system using complex adaptive system concepts. In: Proceedings of the 2nd International Conference on Computing and Wireless Communication Systems, p. 22. ACM (2017)","DOI":"10.1145\/3167486.3167508"},{"issue":"4","key":"17_CR22","doi-asserted-by":"crossref","first-page":"2045","DOI":"10.11591\/ijece.v7i4.pp2045-2053","volume":"7","author":"A Jarrar","year":"2017","unstructured":"Jarrar, A., Balouki, Y., Gadi, T.: Formal specification of QoS negotiation in ODP system. Int. J. Electric. Comput. Eng. 7(4), 2045 (2017)","journal-title":"Int. J. Electric. Comput. Eng."},{"key":"17_CR23","first-page":"478","volume-title":"IFIP Advances in Information and Communication Technology","author":"Hafid Belhaj","year":"2010","unstructured":"Belhaj, H., Balouki, Y., Bouhdadi, M., El Hajji, S.: Using event B to specify QoS in ODP enterprise language. In: Working Conference on Virtual Enterprises, pp. 478\u2013485. Springer, Berlin, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2018"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95165-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T14:50:49Z","timestamp":1751727049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95165-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319951645","9783319951652"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95165-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}