{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:05:40Z","timestamp":1761487540662},"publisher-location":"Boston","reference-count":15,"publisher":"Kluwer Academic Publishers","isbn-type":[{"type":"print","value":"1402081480"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8149-9_8","type":"book-chapter","created":{"date-parts":[[2006,2,22]],"date-time":"2006-02-22T14:53:33Z","timestamp":1140620013000},"page":"73-82","source":"Crossref","is-referenced-by-count":1,"title":["Temporal Bounds for TTA : Validation"],"prefix":"10.1007","author":[{"given":"K.","family":"Godary","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I.","family":"Aug\u00e9-Blum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Mignotte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Bauer, G. and Kopetz, H. (2000). Transparent redundancy in the time-triggered architecture. In Int. Conf. on Dependable Systems and Networks (DSN 2000), New York, New York.","DOI":"10.1109\/ICDSN.2000.857508"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Bengtsson, J. and Yi, W. (2004). Timed automata: Semantics, algorithms and tools. Uppsala University.","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A. and Merceron, A. (2002). Parametric verification of a group membership algorithm. In 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT\u201902), volume LNCS 2469, pages 311\u2013330, Oldenburg (Germany).","DOI":"10.1007\/3-540-45739-9_19"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Caspi, P., Curie, A., Maignan, A., Sofronis, C., Tripakis, S., and Niebert, P. (2003). From simulink to scade\/lustre to tta: a layered approach for distributed embedded applications. In Proc. of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, pages 153\u2013162. ACM Press.","DOI":"10.1145\/780732.780754"},{"key":"8_CR5","unstructured":"Blum, I., and Mignotte, A. (2004a). Evaluation of model abstractions for the temporal validation of tta with uppaal. Technical Report RR2004-2, Lab. CITI, INSA Lyon."},{"key":"8_CR6","unstructured":"Blum, I., and Mignotte, A. (2004b). Sdl and timed petri nets versus uppaal for the validation of embedded architecture in automotive. Technical Report RR2004-1, Lab. CITI, INSA Lyon."},{"key":"8_CR7","volume-title":"Modelling and analysis of a collision avoidance protocol using spin and uppaal","author":"H. E. Jensen","year":"1996","unstructured":"Jensen, H. E., Larsen, K. G., and Skou, A. (1996). Modelling and analysis of a collision avoidance protocol using spin and uppaal. In In Proc. of the 2nd SPIN Workshop, New Jersey, USA. Rutgers University."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Kopetz, H. (1998). The time-triggered architecture. In IEEE Int. Symp. on Object-Oriented Real-Time Distributed Computing (ISORC\u201998), volume LNCS 2469, Kyoto, Japan.","DOI":"10.1109\/ISORC.1998.666765"},{"issue":"1","key":"8_CR9","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"Larsen, K., Pettersson, P., and Yi, W. (1997). UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1):134\u2013152.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"8_CR10","unstructured":"Lindahl, M., Pettersson, P., and Yi, W. (1998). Formal Design and Analysis of a Gear-Box Controller. In Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS. Springer-Verlag."},{"key":"8_CR11","unstructured":"L\u00f6nn, H. and Pettersson, P. (1997). Formal Verification of a TDMA Protocol Startup Mechanism. In Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, pages 235\u2013242."},{"key":"8_CR12","unstructured":"Pettersson, P. (1999). Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. Phdthesis-technical report docs 99\/101, Department of Computer Systems, Uppsala University."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Pfeifer, H. (2000). Formal verification of the ttp group membership algorithm. In IFIP, Int. Conf. on Formal Description Techniques for Distributed Systems and Communication protocols and Protocol Specification, Testing and Verification, FORTE\/PSTV 2000, Pisa, Italy.","DOI":"10.1007\/978-0-387-35533-7_1"},{"key":"8_CR14","volume-title":"PhD thesis","author":"H. Pfeifer","year":"2003","unstructured":"Pfeifer, H. (2003). Formal Analysis of Fault-Tolerant Algorithms in the Time-Triggered Architecture. PhD thesis, Universitat Ulm, Germany."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Rushby, J. (2002). An overview of formal verification for the time-triggered architecture. In Damm, W. and Olderog, E.-R., editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, Oldenburg, Germany. Springer-Verlag.","DOI":"10.1007\/3-540-45739-9_7"}],"container-title":["IFIP International Federation for Information Processing","Design Methods and Applications for Distributed Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8149-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:28:41Z","timestamp":1619555321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8149-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081480"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8149-9_8","relation":{},"subject":[]}}