{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:27:23Z","timestamp":1761596843005},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1007\/s10009-003-0107-8","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T14:26:30Z","timestamp":1079792790000},"page":"456-471","source":"Crossref","is-referenced-by-count":9,"title":["Generating online test oracles from temporal logic specifications"],"prefix":"10.1007","volume":"4","author":[{"given":"John","family":"H\u00e5kansson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ola","family":"Lundqvist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,8,1]]},"reference":[{"key":"107_CR1","doi-asserted-by":"crossref","unstructured":"Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) FoCS: Automatic generation of simulation checkers from formal specifications. In: Emerson, Sistla (eds) Proc. 12th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1855. Springer, Berlin Heidelberg New York, pp 538\u2013542","DOI":"10.1007\/10722167_40"},{"key":"107_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger T (1989) A really temporal logic. In: Proc. 30th Annual Symp. Foundations of Computer Science, pp 164\u2013169","DOI":"10.1109\/SFCS.1989.63473"},{"key":"107_CR3","doi-asserted-by":"crossref","unstructured":"Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: Proc. 11th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science vol. 1633. Springer, Berlin Heidelberg New York, pp 249\u2013260","DOI":"10.1007\/3-540-48683-6_23"},{"key":"107_CR4","doi-asserted-by":"crossref","unstructured":"Drusinsky D (2000) The temporal rover and the ATG rover. In: Havelund K (ed) SPIN Model Checking and Software Verification, Proc. 7th SPIN Workshop, Lecture Notes in Computer Science vol. 1885. Springer, Berlin Heidelberg New York, Stanford, Calif., USA, pp 323\u2013330","DOI":"10.1007\/10722468_19"},{"key":"107_CR5","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proc. 21st Int. Conf. on Software Engineering. IEEE Computer Society, New York, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"107_CR6","doi-asserted-by":"crossref","unstructured":"Etessami K, Holzmann G (2000) Optimizing B\u00fcchi automata. In: Palamidessi C (ed) Proc. CONCUR 2000 11th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, vol. 1877. Springer, Berlin Heidelberg New York, pp 153\u2013167","DOI":"10.1007\/3-540-44618-4_13"},{"key":"107_CR7","doi-asserted-by":"crossref","unstructured":"Felder M, Morzenti A (1994) Validating real-time systems by history-checking TRIO specifications. ACM Trans Software Eng Method 3(4):308\u2013339","DOI":"10.1145\/201024.201034"},{"key":"107_CR8","doi-asserted-by":"crossref","unstructured":"Fisher M (1997) A normal form for temporal logics and its applications in theorem-proving and execution. J Logic Comput 7(4):429\u2013456","DOI":"10.1093\/logcom\/7.4.429"},{"key":"107_CR9","doi-asserted-by":"crossref","unstructured":"Gastin P, Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: Berry, Comon, Finkel (eds) Proc. 13th Int. Conf. on Computer Aided Verification Lecture Notes in Computer Science, vol. 2102. Springer, Berlin Heidelberg New York, pp 53\u201365","DOI":"10.1007\/3-540-44585-4_6"},{"key":"107_CR10","unstructured":"H\u00e5kansson J (2000) Automated generation of test scripts from temporal logic specifications. Master\u2019s thesis, Uppsala University"},{"key":"107_CR11","doi-asserted-by":"crossref","unstructured":"Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: Katoen JP, Stevens P (eds) Proc. TACAS \u201902 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science vol. 2280. Springer, Berlin Heidelberg New York, pp 324\u2013356","DOI":"10.1007\/3-540-46002-0_24"},{"key":"107_CR12","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng SE-23(5):279\u2013295","DOI":"10.1109\/32.588521"},{"key":"107_CR13","doi-asserted-by":"crossref","unstructured":"Kesten Y, Manna Z, McGuire H, Pnueli A (1993) A decision algorithm for full propositional temporal logic. In: Courcoubetis (ed) Proc. 5th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science vol. 697. Springer, Berlin Heidelberg New York, pp 97\u2013109","DOI":"10.1007\/3-540-56922-7_9"},{"key":"107_CR14","doi-asserted-by":"crossref","unstructured":"Kesten Y, Pnueli A, Raviv L (1998) Algorithmic verification of linear temporal logic specifications. In: Proc. ICALP \u201998 25th International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science vol. 1443. Springer, Berlin Heidelberg New York, pp 1\u201316","DOI":"10.1007\/BFb0055036"},{"key":"107_CR15","doi-asserted-by":"crossref","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125\u2013143","DOI":"10.1109\/TSE.1977.229904"},{"key":"107_CR16","doi-asserted-by":"crossref","unstructured":"Mandrioli D, Morasca S, Morzenti A (1995) Generating test cases for real-time systems from logic specifications. ACM Trans Comput Syst 13(4):365\u2013398","DOI":"10.1145\/210223.210226"},{"key":"107_CR17","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"107_CR18","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"107_CR19","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic, Boston, Mass., USA","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"107_CR20","unstructured":"Nielsen J (1998) Real-time specification using the TRIO language. Master\u2019s thesis, Royal Institute of Technology Stockholm"},{"key":"107_CR21","unstructured":"O\u2019Malley TO, Richardson DJ, Dillon LK (1996) Efficient specification-based test oracles for critical systems. In: Proc. California Software Symposium, April"},{"key":"107_CR22","doi-asserted-by":"crossref","unstructured":"Ouabdesselam F, Parissis I (1994) Testing synchronous critical software. In: Proc. 5th Int. Symp. on Software Reliability Engineering, Monterey, Calif., USA, November, pp 239\u2013248","DOI":"10.1109\/ISSRE.1994.341380"},{"key":"107_CR23","doi-asserted-by":"crossref","unstructured":"Parissis I, Ouabdesselam F (1996) Specification-based testing of synchronous software. In: Proc. 4th ACM SIGSOFT Symp. on Foundations of Software Engineering. ACM, New York, pp 127\u2013134","DOI":"10.1145\/239098.239119"},{"key":"107_CR24","doi-asserted-by":"crossref","unstructured":"Peters DK, Parnas DL (1998) Using test oracles generated from program documentation. IEEE Trans Softw Eng 24(3):161\u2013173","DOI":"10.1109\/32.667877"},{"key":"107_CR25","doi-asserted-by":"crossref","unstructured":"Raymond P, Nicollin X, Halbwachs N, Weber D (1998) Automatic testing of reactive systems. In: Proc. 19th IEEE Real-Time Systems Symposium. IEEE Computer Society, New York, pp 200\u2013209","DOI":"10.1109\/REAL.1998.739746"},{"key":"107_CR26","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. In: Proc. 12th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, vol 1855. Springer, Berlin Heidelberg New York, pp 247\u2013263","DOI":"10.1007\/10722167_21"},{"key":"107_CR27","unstructured":"Vardi M.Y, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proc. LICS \u201986 1st IEEE Int. Symp. on Logic in Computer Science, June, pp 332\u2013344"}],"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-003-0107-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0107-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0107-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0107-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:17Z","timestamp":1559114717000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0107-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["107"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0107-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}