{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T01:40:12Z","timestamp":1736646012920,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482659"},{"type":"electronic","value":"9783540482673"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916246_7","type":"book-chapter","created":{"date-parts":[[2006,11,22]],"date-time":"2006-11-22T08:01:36Z","timestamp":1164182496000},"page":"133-152","source":"Crossref","is-referenced-by-count":0,"title":["Achieving Fault Tolerance by a Formally Validated Interaction Policy"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Semini","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"ENTCS","first-page":"161","volume-title":"1st International Workshop on Automated Specification and Verification of Web sites (WWV 2005)","author":"G. Amato","year":"2005","unstructured":"Amato, G., Coppola, M., Gnesi, S., Scozzari, F., Semini, L.: Modeling web applications by the multiple levels of integrity policy. In: Falaschi, M., Alpuente, M., Escobar, S. (eds.) 1st International Workshop on Automated Specification and Verification of Web sites (WWV 2005), Valencia, Spain, March 14-15, 2005. ENTCS, vol.\u00a0157(2), pp. 161\u2013176. Elsevier Science, Amsterdam (2005)"},{"key":"7_CR2","unstructured":"Bell, D.E., LaPadula, L.J.: Security Computer Systems: Mathematical foundations and model. Technical Report Technical Report M74-244, MITRE Corp., Bedford, Mass. (1974)"},{"issue":"3","key":"7_CR3","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0951-8320(00)00078-8","volume":"71","author":"C. Bernardeschi","year":"2001","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S.: Formal Validation of the GUARDS Inter\u2013consistency Mechanism. Reliability, Engineering and System Safety (RE&SS)\u00a071(3), 261\u2013270 (2001)","journal-title":"Reliability, Engineering and System Safety (RE&SS)"},{"issue":"4","key":"7_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1002\/stvr.258","volume":"12","author":"C. Bernardeschi","year":"2002","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S.: Model checking fault tolerant systems. Software Testing, Verification & Reliability (STVR)\u00a012(4), 251\u2013275 (2002)","journal-title":"Software Testing, Verification & Reliability (STVR)"},{"key":"7_CR5","series-title":"ACM Software Engineering Notes","first-page":"140","volume-title":"Proc. ACM SIGSOFT 8th Int. Symp. on the Foundations of Software Engineering (FSE-2000)","author":"M. Bernardo","year":"2000","unstructured":"Bernardo, M., Ciancarini, P., Donatiello, L.: On the Formalization of Architectural Types with Process Algebras. In: Proc. ACM SIGSOFT 8th Int. Symp. on the Foundations of Software Engineering (FSE-2000). ACM Software Engineering Notes, vol.\u00a025(6), pp. 140\u2013148. ACM Press, New York (2000)"},{"key":"7_CR6","unstructured":"Biba, K.: Integrity Considerations for Secure Computer Systems. Technical Report Tech. Rep. ESD-TR 76-372, MITRE Co. (April 1997)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BFb0000462","volume-title":"Algebraic Methodology and Software Technology","author":"G. Bruns","year":"1997","unstructured":"Bruns, G., Sutherland, I.: Model Checking and Fault Tolerance. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol.\u00a01349, pp. 45\u201359. Springer, Heidelberg (1997)"},{"key":"7_CR8","first-page":"184","volume-title":"IEEE Symp. on Security and Privacy","author":"D.D. Clark","year":"1987","unstructured":"Clark, D.D., Wilson, D.R.: Comparison of Commercial and Military Computer Security Policies. In: IEEE Symp. on Security and Privacy, Oakland, CA, pp. 184\u2013194. IEEE Computer Society Press, Los Alamitos (1987)"},{"key":"7_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R. Nicola De","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.W.: Action versus State based Logics for Transition Systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol.\u00a0469, pp. 407\u2013419. Springer, Heidelberg (1990)"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and Not Never Revisited: on Branching Time versus Linear Time Temporal Logic. Journal of ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of ACM"},{"key":"7_CR12","unstructured":"Fantechi, A., Gnesi, S., Semini, L.: Applications of formal methods for validating an interaction policy. Technical Report ISTI\u20132004\u2013TR\u201359, ISTI\u2013CNR (2004)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Fraser, T.: LOMAC: Low Water-Mark Integrity Protection for COTS Environments. In: IEEE Symposium on Security and Privacy, pp. 230\u2013245 (2000)","DOI":"10.1109\/SECPRI.2000.848460"},{"key":"7_CR14","unstructured":"Gnesi, S., Mazzanti, F.: On the Fly Verification of Networks of Automata. In: Proc. Int. Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999, special session on Current limits to automated verification for distributed systems, Las Vegas, Ne, June 1999. CSREA Press (1999)"},{"key":"7_CR15","series-title":"Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall Int., Englewood Cliffs (1985)"},{"issue":"23","key":"7_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"5","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker SPIN. IEEE Transaction on Software Engineering\u00a05(23), 279\u2013295 (1997)","journal-title":"IEEE Transaction on Software Engineering"},{"key":"7_CR17","volume-title":"The SPIN model checker: Primer and reference manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN model checker: Primer and reference manual. Addison-Wesley, Reading (2004)"},{"issue":"1","key":"7_CR18","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/314602.314605","volume":"21","author":"Z. Liu","year":"1999","unstructured":"Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. Program. Lang. Syst.\u00a021(1), 46\u201389 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR19","series-title":"International Series in Computer Science","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"5","key":"7_CR20","doi-asserted-by":"publisher","first-page":"914","DOI":"10.1145\/330249.330251","volume":"21","author":"B.C. Pierce","year":"1999","unstructured":"Pierce, B.C., Kobayashi, N., Turner, D.N.: Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems\u00a021(5), 914\u2013947 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR21","volume-title":"Proceedings of FORTE\/PSTV 1999","author":"E. Najm","year":"1999","unstructured":"Najm, E., Nimour, A., Stefani, J.-B.: Garanteeing liveness in an object calculus through behavioral typing. In: Proceedings of FORTE\/PSTV 1999, Beijing, China, October 1999. Kluwer, Dordrecht (1999)"},{"key":"7_CR22","first-page":"99","volume-title":"Regular types for active object","author":"O. Nierstrasz","year":"1995","unstructured":"Nierstrasz, O.: Regular types for active object, pp. 99\u2013121. Prentice-Hall, Englewood Cliffs (1995)"},{"volume-title":"A Generic Fault\u2013Tolerant Architecture for Real\u2013Time Dependable Systems","year":"2001","key":"7_CR23","unstructured":"Powell, D. (ed.): A Generic Fault\u2013Tolerant Architecture for Real\u2013Time Dependable Systems, January 2001. Kluwer Academic Publishers, Dordrecht (2001)"},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1109\/DSN.2004.1311889","volume-title":"The International Conference on Dependable Systems and Networks","author":"W. Steiner","year":"2004","unstructured":"Steiner, W., Rushby, J., Sorea, M., Pfeifer, H.: Model checking a fault-tolerant startup algorithm: From design exploration to exhaustive fault simulation. In: The International Conference on Dependable Systems and Networks, Florence, Italy, June 2004, pp. 189\u2013198. IEEE Computer Society, Los Alamitos (2004)"},{"key":"7_CR25","unstructured":"Totel, E., Beus-Dukic, L., Blanquart, J.-P., Deswarte, Y., Nicomet, V., Powell, D., Wellings, A.: Multi level integrity mechanism. ch. 6 of [23]"},{"key":"7_CR26","volume-title":"Proceedings 28th Int. Symp. on Fault-Tolerant Computing (FTCS-28)","author":"E. Totel","year":"1998","unstructured":"Totel, E., Blanquart, J.-P., Deswarte, Y., Powell, D.: Supporting Multiple Levels of Criticality. In: Proceedings 28th Int. Symp. on Fault-Tolerant Computing (FTCS-28), Munich, Germany, June 1998. IEEE Computer Society Press, Los Alamitos (1998)"}],"container-title":["Lecture Notes in Computer Science","Rigorous Development of Complex Fault-Tolerant Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11916246_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T01:25:23Z","timestamp":1736645123000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916246_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482659","9783540482673"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11916246_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}