{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T04:29:00Z","timestamp":1742012940129,"version":"3.38.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2011,12,8]],"date-time":"2011-12-08T00:00:00Z","timestamp":1323302400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10009-011-0220-z","type":"journal-article","created":{"date-parts":[[2011,12,7]],"date-time":"2011-12-07T16:22:47Z","timestamp":1323274967000},"page":"407-437","source":"Crossref","is-referenced-by-count":5,"title":["More testable properties"],"prefix":"10.1007","volume":"14","author":[{"given":"Yli\u00e8s","family":"Falcone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Claude","family":"Fernandez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"J\u00e9ron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Herv\u00e9","family":"Marchand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,12,8]]},"reference":[{"issue":"4","key":"220_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern B., Schneider F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"220_CR2","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3) (2010)","DOI":"10.1093\/logcom\/exn075"},{"key":"220_CR3","doi-asserted-by":"crossref","unstructured":"Cern\u00e1, I., Pel\u00e1nek, R.: Relating the hierarchy of temporal properties to model checking. In: MFCS 2003: Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 2747, pp. 318\u2013327. Springer (2003)","DOI":"10.1007\/978-3-540-45138-9_26"},{"key":"220_CR4","doi-asserted-by":"crossref","unstructured":"Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623, pp. 474\u2013486. Springer (1992)","DOI":"10.1007\/3-540-55719-9_97"},{"key":"220_CR5","doi-asserted-by":"crossref","unstructured":"Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. Technical report, Stanford University, Department of Computer Science (1992)","DOI":"10.1007\/978-3-642-58041-3_5"},{"issue":"8","key":"220_CR6","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1109\/TSE.2007.70707","volume":"33","author":"C. Constant","year":"2007","unstructured":"Constant C., J\u00e9ron T., Marchand H., Rusu V.: Integrating formal verification and conformance testing for reactive systems. IEEE Trans. Softw. Eng. 33(8), 558\u2013574 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"220_CR7","first-page":"341","volume-title":"TestCom. Lecture Notes in Computer Science, vol. 3964","author":"V. Darmaillacq","year":"2006","unstructured":"Darmaillacq V., Fernandez J.-C., Groz R., Mounier L., Richier J.-L.: Test generation for network security rules. In: \u00dcmit Uyar, M., Duale, A.Y., Fecko, M.A. (eds) TestCom. Lecture Notes in Computer Science, vol. 3964, pp. 341\u2013356. Springer, Berlin (2006)"},{"key":"220_CR8","doi-asserted-by":"crossref","unstructured":"Darmaillacq, V., Richier, J.-L., Groz, R.: Test generation and execution for security rules in temporal logic. In: ICSTW \u201908: Proceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, pp. 252\u2013259. IEEE Computer Society (2008)","DOI":"10.1109\/ICSTW.2008.41"},{"key":"220_CR9","unstructured":"de Vries, R.G.: Towards formal test purposes. In: Tretmans, J., Brinksma, Ed. (eds.) FATES\u201901: Formal Approaches to Testing of Software. BRICS Notes Series, pp. 61\u201376 (2001)"},{"key":"220_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science. Formal Models and Sematics (B), vol. B, pp. 995\u20131072. MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"220_CR11","first-page":"30","volume-title":"ICTSS. Lecture Notes in Computer Science, vol. 6435","author":"Y. Falcone","year":"2010","unstructured":"Falcone Y., Fernandez J.-C., J\u00e9ron T., Marchand H., Mounier L.: More testable properties. In: Petrenko, A., da Silva Sim\u00e3o, A., Maldonado, J.C. (eds) ICTSS. Lecture Notes in Computer Science, vol. 6435, pp. 30\u201346. Springer, Berlin (2010)"},{"key":"220_CR12","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: The 9th Int. Workshop on Runtime Verification. Lecture Notes in Computer Science, vol. 5779, pp. 40\u201359. Springer (2009)","DOI":"10.1007\/978-3-642-04694-0_4"},{"key":"220_CR13","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Softw. Tools Technol. Transfer (2011). doi: 10.1007\/s10009-011-0196-8","DOI":"10.1007\/s10009-011-0196-8"},{"key":"220_CR14","first-page":"55","volume-title":"FATES\/RV. Lecture Notes in Computer Science, vol. 4262","author":"Y. Falcone","year":"2006","unstructured":"Falcone Y., Fernandez J.-C., Mounier L., Richier J.-L.: A test calculus framework applied to network security policies. In: Havelund, K., N\u00fa\u00f1ez, M., Rosu, G., Wolff, B. (eds) FATES\/RV. Lecture Notes in Computer Science, vol. 4262, pp. 55\u201369. Springer, Berlin (2006)"},{"key":"220_CR15","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L., Richier, J.-L.: A compositional testing framework driven by partial specifications. In: TestCom\/FATES. Lecture Notes in Computer Science, vol. 4581, pp. 107\u2013122. Springer (2007)","DOI":"10.1007\/978-3-540-73066-8_8"},{"key":"220_CR16","first-page":"147","volume-title":"FATES. Lecture Notes in Computer Science, vol. 2931","author":"J.-C. Fernandez","year":"2003","unstructured":"Fernandez J.-C., Mounier L., Pachon C.: Property oriented test case generation. In: Petrenko, A., Ulrich, A. (eds) FATES. Lecture Notes in Computer Science, vol. 2931, pp. 147\u2013163. Springer, Berlin (2003)"},{"key":"220_CR17","unstructured":"Grabowski, Jens: SDL and MSC based test case generation\u2014an overall view of the SAMSTAG method. Technical report, University of Berne, IAM-94-0005 (1994)"},{"issue":"4","key":"220_CR18","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s10009-004-0153-x","volume":"7","author":"C. Jard","year":"2005","unstructured":"Jard C., J\u00e9ron T.: TGV: theory, principles and algorithms. Softw. Tools Technol. Transfer 7(4), 297\u2013315 (2005)","journal-title":"Softw. Tools Technol. Transfer"},{"key":"220_CR19","doi-asserted-by":"crossref","unstructured":"Koch, B., Grabowski, J., Hogrefe, D., Schmitt, M. II: Autolink: a tool for automatic test generation from SDL specifications. In: WIFT, p. 114. IEEE Computer Society (1998)","DOI":"10.1109\/WIFT.1998.766305"},{"issue":"2","key":"220_CR20","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"220_CR21","doi-asserted-by":"crossref","unstructured":"Machado, P.D.L., Silva, D.A., Mota, A.C.: Towards property oriented testing. In: Proceedings of the Second Brazilian Symposium on Formal Methods (SBMF 2005). Electron. Notes Theor. Comput. Sci., vol. 184, pp. 3\u201319. Elsevier, Amsterdam (2007)","DOI":"10.1016\/j.entcs.2007.06.001"},{"key":"220_CR22","doi-asserted-by":"crossref","unstructured":"Mallouli, W., Orset, J.-M., Cavalli, A., Cuppens, N., Cuppens, F.: A formal approach for testing security rules. In: SACMAT \u201907: Proceedings of the 12th ACM symposium on Access Control Models and Technologies, pp. 127\u2013132. ACM, New York (2007)","DOI":"10.1145\/1266840.1266860"},{"key":"220_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: PODC\u201990: Proceedings of the 9th Symposium on Principles of Distributed Computing, pp. 377\u2013410. ACM, New York (1990)","DOI":"10.1145\/93385.93442"},{"key":"220_CR24","doi-asserted-by":"crossref","unstructured":"Marchand, H., Dubreil, J., J\u00e9ron, T.: Automatic testing of access control for security properties. In: TestCom\/FATES\u201909. Lecture Notes in Computer Science, vol. 5826, pp. 113\u2013128. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-05031-2_8"},{"key":"220_CR25","unstructured":"Nahm, R., Grabowski, J., Hogrefe, D.: Test case generation for temporal properties. Technical report, Bern University (1993)"},{"key":"220_CR26","doi-asserted-by":"crossref","unstructured":"Pecheur, C., Raimondi, F., Brat, G.: A formal analysis of requirements-based testing. In: ISSTA\u201909: Proceedings of the 18th International Symposium on Software Testing and Analysis, pp. 47\u201356. ACM, New York (2009)","DOI":"10.1145\/1572272.1572279"},{"key":"220_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: FM06: Proceedings of the 14th Int. Symp. on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 573\u2013586. Springer, New York (2006)","DOI":"10.1007\/11813040_38"},{"key":"220_CR28","doi-asserted-by":"crossref","unstructured":"Rajan, A., Whalen, M.W., Heimdahl, M.R.: Model validation using automatically generated requirements-based tests. In: HASE \u201907: 10th IEEE Symposium on High Assurance Systems Engineering, pp. 95\u2013104. IEEE Computer Society (2007)","DOI":"10.1109\/HASE.2007.57"},{"key":"220_CR29","doi-asserted-by":"crossref","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse. In: STOC \u201981: Proceedings of the 13th Symp. on Theory of Computing, pp. 375\u2013383. ACM, New York (1981)","DOI":"10.1145\/800076.802492"},{"key":"220_CR30","doi-asserted-by":"crossref","unstructured":"Traon, Y.L., Mouelhi, T., Baudry, B.: Testing security policies: going beyond functional testing. In: 18th IEEE Int. Symp. on Software Reliability Engineering, pp. 93\u2013102, Los Alamitos, CA, USA. IEEE Computer Society (2007)","DOI":"10.1109\/ISSRE.2007.27"},{"key":"220_CR31","unstructured":"Tretmans, J.: A formal approach to conformance testing. In: Rafiq, O. (ed.) Protocol Test Systems. IFIP Transactions, vol. C-19, pp. 257\u2013276. North-Holland (1993)"},{"key":"220_CR32","first-page":"127","volume-title":"TACAS. Lecture Notes in Computer Science, vol. 1055","author":"J. Tretmans","year":"1996","unstructured":"Tretmans J.: Test generation with inputs, outputs, and quiescence. In: Margaria, T., Steffen, B. (eds) TACAS. Lecture Notes in Computer Science, vol. 1055, pp. 127\u2013146. Springer, Berlin (1996)"}],"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-011-0220-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0220-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0220-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T02:25:53Z","timestamp":1742005553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0220-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,8]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["220"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0220-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,12,8]]}}}