{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:31Z","timestamp":1740107971464,"version":"3.37.3"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,6,25]],"date-time":"2014-06-25T00:00:00Z","timestamp":1403654400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10009-014-0327-0","type":"journal-article","created":{"date-parts":[[2014,6,24]],"date-time":"2014-06-24T13:02:49Z","timestamp":1403614969000},"page":"335-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Program verification and testing technologies"],"prefix":"10.1007","volume":"16","author":[{"given":"Tiziana","family":"Margaria","sequence":"first","affiliation":[]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[]},{"given":"Hongli","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,6,25]]},"reference":[{"key":"327_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis,C., Henzinger, T., Ho,P.: Hybrid automata: an algorithmic approach to the specification and analysis of hybrid systems. In: Hybrid Systems. LNCS, vol. 736, pp. 209\u2013229. Springer, Berlin (1993)","DOI":"10.1007\/3-540-57318-6_30"},{"key":"327_CR2","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Ho, P., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 110\u2013122 (1997)","DOI":"10.1007\/s100090050008"},{"key":"327_CR3","doi-asserted-by":"crossref","unstructured":"Frehse, G. : Phaver: algorithmic verification of hybrid systems past hytech. In: HSCC, LNCS, vol. 3414, pp. 258\u2013273. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"327_CR4","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1, 2), 134\u2013152 (1997). http:\/\/dx.doi.org\/10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"327_CR5","unstructured":"Mathworks, I.: Stateflow. http:\/\/www.mathworks.de\/products\/stateflow\/"},{"key":"327_CR6","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno,C., OHearn,P.: Smallfoot: modular automatic assertion checking with separation logic. In: FMCO. LNCS, vol. 4111, pp. 115\u2013137. Springer, Berlin (2006)","DOI":"10.1007\/11804192_6"},{"key":"327_CR7","unstructured":"OHearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL, 2004, Venice, Italy"},{"key":"327_CR8","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman,G., Parker, D.: Stochastic model checking. In: Formal Methods for the Design of Computer, Communication and Software Systems. LNCS, vol. 4486, pp. 220\u2013270. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"327_CR9","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: Verification of probabilistic real-time systems. In: 23rd International Conference on Computer Aided Verification(CAV\u201911). LNCS, vol. 6806, pp. 585\u2013591. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"327_CR10","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker mrmc. Perform. Eval. 68(2), 90\u2013104 (2011). doi: 10.1016\/j.peva.2010.04.001","DOI":"10.1016\/j.peva.2010.04.001"},{"key":"327_CR11","doi-asserted-by":"crossref","unstructured":"Krenn, W., Schlick, R., Aichernig, B.: Mapping uml to labeled transition systems for test-case generation. In: 8th International Symposium on Formal Methods for Components and Objects, pp. 186\u2013207. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-17071-3_10"},{"key":"327_CR12","unstructured":"Raffelt, H., Merten, M., Steffen, B., Margaria, T.: Dynamic testing via automata. Int. J. Softw. Tools Technol. Transf. 11(4), 307\u2013324 (2009)"},{"key":"327_CR13","doi-asserted-by":"crossref","unstructured":"Berg, T., Grinchtein, O., Jonsson, B., Leucker, M., Raffelt, H., Steffen, B.: On the correspondence between conformance testing and regular inference. In: FASE, : ser. LNCS, vol. 3442, pp. 175\u2013189. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31984-9_14"},{"key":"327_CR14","doi-asserted-by":"crossref","unstructured":"Fang, H., Shi, J., Zhu, H., Guo, J., Larsen, K.G., David, A.: Formal verification and simulation for platform screen doors and collision avoidance in subway control systems. Int. J. Softw. Tools Technol. Transf. (this volume). doi: 10.1007\/s10009-014-0318-1","DOI":"10.1007\/s10009-014-0318-1"},{"key":"327_CR15","doi-asserted-by":"crossref","unstructured":"Gherghina, C., David, C., Qin, S., Chin, W.-N.: Expressive program verification via structured specifications. Int. J. Softw. Tools Technol. Transf. (this volume). doi: 10.1007\/s10009-014-0306-5","DOI":"10.1007\/s10009-014-0306-5"},{"key":"327_CR16","doi-asserted-by":"crossref","unstructured":"Ferreira, J.F., Gherghina, C., He, G., Qin, S., Chin, W.-N.: Automated verification of the freertos scheduler in hip\/sleek. Int. J. Softw. Tools Technol. Transf. (this volume). doi: 10.1007\/s10009-014-0307-4","DOI":"10.1007\/s10009-014-0307-4"},{"key":"327_CR17","doi-asserted-by":"crossref","unstructured":"Jarraya, Y., Debbabi, M.: Quantitative and qualitative analysis of sysml activity diagrams. Int. J. Softw. Tools Technol. Transf. (this volume). doi: 10.1007\/s10009-014-0305-6","DOI":"10.1007\/s10009-014-0305-6"},{"key":"327_CR18","doi-asserted-by":"crossref","unstructured":"Y\u00fcksel, E., Nielson, H.R., Nielson, F., Zhu, H., Huang, H.: Quantitative modelling and analysis of a Chinese Smart Grid: a stochastic model checking case study. Int. J. Softw. Tools Technol. Transf. (this volume). doi: 10.1007\/s10009-014-0311-8","DOI":"10.1007\/s10009-014-0311-8"},{"key":"327_CR19","doi-asserted-by":"crossref","unstructured":"Guo, H.-F., Subramaniam, M.: Model-based test generation using extended symbolic grammars. Int. J. Softw. Tools Technol. Transf. (this volume). doi: 10.1007\/s10009-014-0316-3","DOI":"10.1007\/s10009-014-0316-3"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0327-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0327-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0327-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T17:48:47Z","timestamp":1565545727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0327-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,25]]},"references-count":19,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["327"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0327-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,6,25]]}}}