{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T13:14:23Z","timestamp":1773148463690,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540521488","type":"print"},{"value":"9783540469056","type":"electronic"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"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":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52148-8_18","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:22:55Z","timestamp":1330186975000},"page":"213-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Specifying, programming and verifying real-time systems using a synchronous declarative language"],"prefix":"10.1007","author":[{"given":"N.","family":"Halbwachs","sequence":"first","affiliation":[]},{"given":"D.","family":"Pilaud","sequence":"additional","affiliation":[]},{"given":"F.","family":"Ouabdesselam","sequence":"additional","affiliation":[]},{"given":"A-C.","family":"Glory","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"18_CR1","unstructured":"Berry G., Couronn\u00e9 P., Gonthier G.: Synchronous programming of reactive systems, an introduction to Esterel. INRIA report nr.647, 1987."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Berry G., Gonthier G.: The synchronous programming language ESTEREL, design, semantics, implementation. INRIA report nr. 327, 1985, to appear in Science of Computer Programming.","DOI":"10.1007\/3-540-15670-4_19"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Caspi P., Halbwachs N., Pilaud D., Plaice J.A.: Lustre a declarative language for programming synchronous systems. Proc. 14th. Annual ACM Symp. on Principles of Programming Languages, Munich, 1987.","DOI":"10.1145\/41625.41641"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Clarke E.M., Emerson E.A., Sistla A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), January 86.","DOI":"10.1145\/5397.5399"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Koymans R., deRoever W.P.: Examples of a real-time temporal logic specification. In The analysis of concurrent systems, Cambridge, September 83, LNCS vol. 207, Springer Verlag, 1985.","DOI":"10.1007\/3-540-16047-7_50"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Milner R.: Calculi for synchrony and asynchrony. Theor. Comp. Sci., vol.28, 1983.","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Moszkowski B., Manna Z.: Reasoning in interval temporal logic. Proc. Workshop on Logics of Programs, LNCS vol. 164, Springer Verlag, 1984.","DOI":"10.1007\/3-540-12896-4_374"},{"key":"18_CR8","unstructured":"Pilaud D., Halbwachs N.: From a synchronous declarative language to a temporal logic dealing with multiform time. Proc. Symposium on Formal Techniques in Real_Time and Fault_Tolerant Systems, Warwick, September 88."},{"key":"18_CR9","unstructured":"Plaice J.A.: S\u00e9mantique et compilation de Lustre, un langage d\u00e9claratif synchrone. PhD. Thesis, Institut National Polytechnique de Grenoble, May 88."},{"key":"18_CR10","unstructured":"Plaice J.A., Halbwachs N.: Lustre-V2 User's guide and reference manual. Technical Report L2, Spectre Project, IMAG, Grenoble, October 87."},{"key":"18_CR11","unstructured":"Rasse A.: CLEO, interpr\u00e9tation de la non correction de programmes sur un mod\u00e8le. Technical Report C10, Spectre Project, IMAG, Grenoble, June 88."},{"key":"18_CR12","unstructured":"Ratel C.: Etude de la conformit\u00e9 d'un programme Lustre et de ses specifications en logique temporelle arborescente. Master Thesis, Institut National Polytechnique de Grenoble, June 88."},{"key":"18_CR13","unstructured":"Richier J.L., Rodriguez C., Sifakis J., Voiron J.: Verification in Xesar of the sliding window protocol. Proc. IFIP WG 6.1 7th. International Conference on Protocol Specification, Testing and Verification, North Holland, Zurich, 1987."},{"key":"18_CR14","unstructured":"Richier J.L., Rodriguez C., Sifakis J., Voiron J.: Xesar user's guide. Technical Report, Spectre Project, IMAG, Grenoble, September 87."},{"key":"18_CR15","unstructured":"Vergamini D.: Verification by means of observational equivalence on automata. INRIA report nr. 501, 1986."},{"key":"18_CR16","unstructured":"Wadge W.W., Ashcroft E.A.: Lucid, the data-flow programming language. Academic Press"}],"container-title":["Lecture Notes in Computer Science","Automatic Verification Methods for Finite State Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52148-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T14:00:30Z","timestamp":1687269630000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52148-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540521488","9783540469056"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-52148-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}