乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:36:04Z","timestamp":1725867364241},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471686"},{"type":"electronic","value":"9783319471693"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_22","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T17:56:23Z","timestamp":1475603783000},"page":"297-314","source":"Crossref","is-referenced-by-count":6,"title":["Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a CBTC System"],"prefix":"10.1007","author":[{"given":"Franco","family":"Mazzanti","sequence":"first","affiliation":[]},{"given":"Alessio","family":"Ferrari","sequence":"additional","affiliation":[]},{"given":"Giorgio O.","family":"Spagnolo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"22_CR1","unstructured":"Accellera, Property Specification Language - Reference Manual - Version 1.01, April 2003. http:\/\/www.eda.org\/vfv\/docs\/psllrm-1.01.pdf"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-15545-6_20","volume-title":"Software, Services, and Systems","author":"MH Beek ter","year":"2015","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 312\u2013328. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-15545-6_20"},{"key":"22_CR3","unstructured":"http:\/\/fmt.isti.cnr.it\/kandisti"},{"issue":"2","key":"22_CR4","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH Beek ter","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119\u2013135 (2011)","journal-title":"Sci. Comput. Program."},{"key":"22_CR5","unstructured":"UMC home site. http:\/\/fmt.isti.cnr.it\/umc"},{"issue":"3","key":"22_CR6","doi-asserted-by":"crossref","first-page":"16:01","DOI":"10.1145\/2211616.2211619","volume":"21","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Trans. Softw. Eng. Methodol. 21(3), 16:01\u201316:46 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-20401-2_18","volume-title":"Rigorous Software Engineering for Service-Oriented Systems","author":"S Gnesi","year":"2011","unstructured":"Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Wirsing, M., H\u00f6lzl, M. (eds.) SENSORIA Project. LNCS, vol. 6582, pp. 390\u2013407. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20401-2_18"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-319-10702-8_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock avoidance in train scheduling: a model checking approach. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 109\u2013123. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-10702-8_8"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-319-06200-6_22","volume-title":"NASA Formal Methods","author":"F Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a deadlock-free train scheduler: a model checking approach. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 264\u2013269. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-06200-6_22"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-39083-3_7","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2016","author":"F Mazzanti","year":"2016","unstructured":"Mazzanti, F.: An experience in ada multicore programming: parallelisation of a model checking engine. In: Bertogna, M., Pinho, L.M., Qui\u00f1ones, E. (eds.) Ada-Europe 2016. LNCS, vol. 9695, pp. 94\u2013109. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-39083-3_7"},{"key":"22_CR11","unstructured":"Holzmann, G.H.: The SPIN Model Checker. Addison-Wesley Pearson Education (2003). ISBN 0-321-22862-6"},{"key":"22_CR12","unstructured":"Verifying Multi-threaded Software with Spin. http:\/\/spinroot.com"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of Computer Aided Verification (CAV 2002) (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"22_CR14","unstructured":"NuSMV: a new symbolic model checker. http:\/\/nusmv.fbk.eu\/"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014). ISBN: 9780262027717","DOI":"10.7551\/mitpress\/9946.001.0001"},{"key":"22_CR16","unstructured":"MCRL2 analysing system behavior. http:\/\/www.mcrl2.org\/"},{"issue":"6","key":"22_CR17","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/s10009-013-0298-6","volume":"16","author":"A Ferrari","year":"2014","unstructured":"Ferrari, A., Spagnolo, G.O., Martelli, G., Menabeni, S.: From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions. STTT 16(6), 647\u2013667 (2014)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:08:09Z","timestamp":1568434089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}