Skip to main content
Erschienen in: Software and Systems Modeling 4/2017

29.12.2015 | Regular Paper

Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols

verfasst von: Dominique Méry, Michael Poppleton

Erschienen in: Software and Systems Modeling | Ausgabe 4/2017

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

State-based formal methods [e.g. Event-B/RODIN (Abrial in Modeling in Event-B—system and software engineering. Cambridge University Press, Cambridge, 2010; Abrial et al. in Int J Softw Tools Technol Transf (STTT) 12(6):447–466, 2010)] for critical system development and verification are now well established, with track records including tool support and industrial applications. The focus of proof-based verification, in particular, is on safety properties. Liveness properties, which guarantee eventual, or converging computations of some requirements, are less well dealt with. Inductive reasoning about liveness is not explicitly supported. Liveness proofs are often complex and expensive, requiring high-skill levels on the part of the verification engineer. Fairness-based temporal logic approaches have been proposed to address this, e.g. TLA Lamport (ACM Trans Program Lang Syst 16(3):872–923, 1994) and that of Manna and Pnueli (Temporal verification of reactive systems—safety. Springer, New York, 1995). We contribute to this technology need by proposing a fairness-based method integrating temporal and first-order logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of Event-B and TLA. Building on our previous work (Méry and Poppleton in Integrated formal methods, 10th international conference, IFM 2013, Turku, Finland, pp 208–222, 2013. doi:10.​1007/​978-3-642-38613-8_​15), we present the method via three example population protocols Angluin et al. (Distrib Comput 18(4):235–253, 2006). These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network and Mobile Ad-Hoc Network algorithms. Our examples present typical liveness and convergence requirements. We prove convergence results for the examples by integrated modelling and proof with Event-B/RODIN and TLA. We exploit existing proof rules, define and apply three new proof rules; soundness proofs are also provided. During the process we observe certain repeating patterns in the proofs. These are easily identified and reused because of the explicit nature of the reasoning.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
We do not consider the hybrid interface of this discrete model to the wireless radio environment.
 
2
Note that the more sophisticated modelling of the hybrid discrete/continuous controller/environment interface offered by the Hybrid Systems community is under active consideration by the Event-B community [9, 2022].
 
3
We will write \(\varPhi _c\) REF \(\varPhi _a\) to abbreviate this.
 
4
\(\textsf {iact}_0\) “anticipates” the interaction in the subsequent refinement \(\textsc {PPM}_1\) by allowing maximal nondeterministic change in \(l\) under the constraint of the invariant and the initial configuration cl. This provides a vehicle against which the behaviour of “anticipated” interaction event \(\textsf {iact}_1\) on \(l\) can simulate defined behaviour in \(\textsc {PPM}_0\). It removes the need for a duplicate variable for \(l\) in a data refinement.
 
5
Keyword convergent for \(\textsf {iact}_1\) generates an inductive PO requiring this variant to be reduced by the event.
 
6
For ease of reading, we gloss over the event artefact required to avoid redundant variables in data refinement, as per \(\textsf {iact}_0\) in Sect. 3.1.
 
Literatur
2.
Zurück zum Zitat Abadi, M., Merz, S.: On TLA as a logic. In: Broy, M. (ed.) NATO ASI DPD, pp. 235–271 (1996) Abadi, M., Merz, S.: On TLA as a logic. In: Broy, M. (ed.) NATO ASI DPD, pp. 235–271 (1996)
3.
Zurück zum Zitat Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefMATH Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefMATH
4.
Zurück zum Zitat Abrial, J.R.: Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH Abrial, J.R.: Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
5.
Zurück zum Zitat Abrial, J.R.: Private communication (2013) Abrial, J.R.: Private communication (2013)
6.
Zurück zum Zitat Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. (STTT) 12(6), 447–466 (2010)CrossRef Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. (STTT) 12(6), 447–466 (2010)CrossRef
7.
Zurück zum Zitat Abrial, J.R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) Proceedings of ICFEM 2006, LNCS, vol. 4260. Macau (2006) Abrial, J.R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) Proceedings of ICFEM 2006, LNCS, vol. 4260. Macau (2006)
8.
Zurück zum Zitat Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) 2nd International B Conference, LNCS, vol. 1393, pp. 83–128. Springer, Montpellier (1998) Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) 2nd International B Conference, LNCS, vol. 1393, pp. 83–128. Springer, Montpellier (1998)
9.
Zurück zum Zitat Abrial, J.R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: ABZ, pp. 178–193 (2012) Abrial, J.R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: ABZ, pp. 178–193 (2012)
11.
Zurück zum Zitat Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRefMATH Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRefMATH
12.
Zurück zum Zitat Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. Distrib. Comput. 18(4), 235–253 (2006)CrossRefMATH Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. Distrib. Comput. 18(4), 235–253 (2006)CrossRefMATH
13.
Zurück zum Zitat Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distrib. Comput. 20(4), 279–304 (2007)CrossRefMATH Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distrib. Comput. 20(4), 279–304 (2007)CrossRefMATH
14.
Zurück zum Zitat Angluin, D., Aspnes, J., Fischer, M.J., Jiang, H.: Self-stabilizing population protocols. TAAS 3(4),103–117 (2008) Angluin, D., Aspnes, J., Fischer, M.J., Jiang, H.: Self-stabilizing population protocols. TAAS 3(4),103–117 (2008)
15.
16.
Zurück zum Zitat Araki, K., Galloway, A., Taguchi, K. (eds.): Integrated Formal Methods, Proceedings of the 1st International Conference on Integrated Formal Methods, IFM 99, New York, UK, 28–29 June 1999. Springer (1999) Araki, K., Galloway, A., Taguchi, K. (eds.): Integrated Formal Methods, Proceedings of the 1st International Conference on Integrated Formal Methods, IFM 99, New York, UK, 28–29 June 1999. Springer (1999)
17.
Zurück zum Zitat Aspnes, J., Ruppert, E.: An introduction to population protocols. Bull. EATCS 93, 98–117 (2007)MathSciNetMATH Aspnes, J., Ruppert, E.: An introduction to population protocols. Bull. EATCS 93, 98–117 (2007)MathSciNetMATH
18.
Zurück zum Zitat Back, R.J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)CrossRefMATH Back, R.J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)CrossRefMATH
19.
Zurück zum Zitat Back, R.J., Kurki-Suonio, R.: Decentralization of process nets with centralized control. Distrib. Comput. 3(2), 73–87 (1989)CrossRef Back, R.J., Kurki-Suonio, R.: Decentralization of process nets with centralized control. Distrib. Comput. 3(2), 73–87 (1989)CrossRef
20.
Zurück zum Zitat Banach, R.: Pliant modalities in hybrid Event-B. In: iu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods, Lecture Notes in Computer Science, vol. 8051, pp. 37–53. Springer (2013) Banach, R.: Pliant modalities in hybrid Event-B. In: iu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods, Lecture Notes in Computer Science, vol. 8051, pp. 37–53. Springer (2013)
21.
Zurück zum Zitat Banach, R., Butler, M.: Cruise control in hybrid Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC, Lecture Notes in Computer Science, vol. 8049, pp. 76–93. Springer (2013) Banach, R., Butler, M.: Cruise control in hybrid Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC, Lecture Notes in Computer Science, vol. 8049, pp. 76–93. Springer (2013)
22.
Zurück zum Zitat Banach, R., Zhu, H., Su, W., Wu, X.: Continuous behaviour in Event-B: A sketch. In: ABZ, pp. 349–352 (2012) Banach, R., Zhu, H., Su, W., Wu, X.: Continuous behaviour in Event-B: A sketch. In: ABZ, pp. 349–352 (2012)
23.
Zurück zum Zitat Beauquier, J., Blanchard, P., Burman, J.: Self-stabilizing leader election in population protocols over arbitrary communication graphs. In: Baldoni, R., Nisse, N., van Steen, M. (eds.) Principles of Distributed Systems—17th International Conference, OPODIS 2013, Nice, France, December 16–18, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8304, pp. 38–52. Springer (2013) Beauquier, J., Blanchard, P., Burman, J.: Self-stabilizing leader election in population protocols over arbitrary communication graphs. In: Baldoni, R., Nisse, N., van Steen, M. (eds.) Principles of Distributed Systems—17th International Conference, OPODIS 2013, Nice, France, December 16–18, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8304, pp. 38–52. Springer (2013)
24.
Zurück zum Zitat Bjorner, D.: Software Engineering 1 Abstraction and Modelling. Springer, Texts in Theoretical Computer Science. An EATCS Series (2006). ISBN 978-3-540-21149-5 Bjorner, D.: Software Engineering 1 Abstraction and Modelling. Springer, Texts in Theoretical Computer Science. An EATCS Series (2006). ISBN 978-3-540-21149-5
25.
Zurück zum Zitat Bjorner, D.: Software Engineering 2 Specification of Systems and Languages. Springer, Texts in Theoretical Computer Science. An EATCS Series (2006). ISBN 978-3-540-21150-1 Bjorner, D.: Software Engineering 2 Specification of Systems and Languages. Springer, Texts in Theoretical Computer Science. An EATCS Series (2006). ISBN 978-3-540-21150-1
26.
Zurück zum Zitat Bjorner, D.: Software Engineering 3 Domains, Requirements, and Software Design. Springer, Texts in Theoretical Computer Science. An EATCS Series (2006). ISBN 978-3-540-21151-8 Bjorner, D.: Software Engineering 3 Domains, Requirements, and Software Design. Springer, Texts in Theoretical Computer Science. An EATCS Series (2006). ISBN 978-3-540-21151-8
27.
Zurück zum Zitat Bjørner, D., Henson, M.C. (eds.): Logics of Specification Languages. EATCS Textbook in Computer Science. Springer, New York (2007) Bjørner, D., Henson, M.C. (eds.): Logics of Specification Languages. EATCS Textbook in Computer Science. Springer, New York (2007)
28.
Zurück zum Zitat Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16–19, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5423, pp. 20–38. Springer (2009) Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16–19, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5423, pp. 20–38. Springer (2009)
29.
Zurück zum Zitat Butler, M.: Towards a cookbook for modelling and refinement of control problems. ECS, University of Southampton, Technical Report (2009) Butler, M.: Towards a cookbook for modelling and refinement of control problems. ECS, University of Southampton, Technical Report (2009)
30.
Zurück zum Zitat Cai, S., Izumi, T., Wada, K.: How to prove impossibility under global fairness: on space complexity of self-stabilizing leader election on a population protocol model. Theory Comput. Syst. 50(3), 433–445 (2012)MathSciNetCrossRefMATH Cai, S., Izumi, T., Wada, K.: How to prove impossibility under global fairness: on space complexity of self-stabilizing leader election on a population protocol model. Theory Comput. Syst. 50(3), 433–445 (2012)MathSciNetCrossRefMATH
31.
Zurück zum Zitat Cansell, D., Méry, D., Merz, S.: Predicate diagrams for the verification of reactive systems. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM, Lecture Notes in Computer Science, vol. 1945, pp. 380–397. Springer (2000) Cansell, D., Méry, D., Merz, S.: Predicate diagrams for the verification of reactive systems. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM, Lecture Notes in Computer Science, vol. 1945, pp. 380–397. Springer (2000)
32.
Zurück zum Zitat Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)MATH Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)MATH
34.
Zurück zum Zitat Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: Giannakopoulou, D., Méry, D. (eds.) FM, Lecture Notes in Computer Science, vol. 7436, pp. 147–154. Springer (2012) Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: Giannakopoulou, D., Méry, D. (eds.) FM, Lecture Notes in Computer Science, vol. 7436, pp. 147–154. Springer (2012)
35.
36.
Zurück zum Zitat Fathabadi, A.S., Butler, M., Rezazadeh, A.: A systematic approach to atomicity decomposition in event-b. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Software Engineering and Formal Methods—10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1–5, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7504, pp. 78–93. Springer (2012). doi:10.1007/978-3-642-33826-7 Fathabadi, A.S., Butler, M., Rezazadeh, A.: A systematic approach to atomicity decomposition in event-b. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Software Engineering and Formal Methods—10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1–5, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7504, pp. 78–93. Springer (2012). doi:10.​1007/​978-3-642-33826-7
37.
Zurück zum Zitat Fischer, M.J., Jiang, H.: Self-stabilizing leader election in networks of finite-state anonymous agents. In: Shvartsman, A.A. (ed.) Principles of Distributed Systems, 10th International Conference, OPODIS 2006, Bordeaux, France, December 12–15, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4305, pp. 395–409. Springer (2006) Fischer, M.J., Jiang, H.: Self-stabilizing leader election in networks of finite-state anonymous agents. In: Shvartsman, A.A. (ed.) Principles of Distributed Systems, 10th International Conference, OPODIS 2006, Bordeaux, France, December 12–15, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4305, pp. 395–409. Springer (2006)
39.
Zurück zum Zitat Gibson, J.P., Méry, D.: A unifying model for specification and design. In: Proceedings of the Workshop on Proof Theory of Concurrent Object-Oriented Programming (1996) Gibson, J.P., Méry, D.: A unifying model for specification and design. In: Proceedings of the Workshop on Proof Theory of Concurrent Object-Oriented Programming (1996)
40.
Zurück zum Zitat Gibson, P., Méry, D.: Fair objects. In: In OT98 COTSR, pp. 245–254 (1997) Gibson, P., Méry, D.: Fair objects. In: In OT98 COTSR, pp. 245–254 (1997)
41.
Zurück zum Zitat Groslambert, J.: Verification of LTL on B event systems. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besançon, France, January 17–19, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4355, pp. 109–124. Springer (2007) Groslambert, J.: Verification of LTL on B event systems. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besançon, France, January 17–19, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4355, pp. 109–124. Springer (2007)
42.
Zurück zum Zitat Hallerstede, S.: On the purpose of Event-B proof obligations. In: E. Börger, M.J. Butler, J.P. Bowen, P. Boca (eds.) Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16–18, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5238, pp. 125–138. Springer (2008) Hallerstede, S.: On the purpose of Event-B proof obligations. In: E. Börger, M.J. Butler, J.P. Bowen, P. Boca (eds.) Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16–18, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5238, pp. 125–138. Springer (2008)
43.
Zurück zum Zitat Hoang, T.S., Abrial, J.R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM, Lecture Notes in Computer Science, vol. 6991, pp. 456–471. Springer (2011) Hoang, T.S., Abrial, J.R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM, Lecture Notes in Computer Science, vol. 6991, pp. 456–471. Springer (2011)
44.
Zurück zum Zitat Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Upper Saddle River (1985)MATH Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Upper Saddle River (1985)MATH
45.
Zurück zum Zitat Hudon, S., Hoang, T.S.: Systems design guided by progress concerns. In: IFM, pp. 16–30 (2013) Hudon, S., Hoang, T.S.: Systems design guided by progress concerns. In: IFM, pp. 16–30 (2013)
46.
Zurück zum Zitat Jackson, M.: System Development. Prentice-Hall, Englewood Cliffs (1983)MATH Jackson, M.: System Development. Prentice-Hall, Englewood Cliffs (1983)MATH
47.
Zurück zum Zitat Järvinen, H.M., Kurki-Suonio, R.: Disco specification language: marriage of actions and objects. In: ICDCS, pp. 142–151. IEEE Computer Society (1991) Järvinen, H.M., Kurki-Suonio, R.: Disco specification language: marriage of actions and objects. In: ICDCS, pp. 142–151. IEEE Computer Society (1991)
48.
Zurück zum Zitat Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983) Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
49.
Zurück zum Zitat Kansal, A., Hsu, J., Zahedi, S., Srivastava, M.B.: Power management in energy harvesting sensor networks. ACM Trans. Embed. Comput. Syst. (2007). doi:10.1145/1274858.1274870 Kansal, A., Hsu, J., Zahedi, S., Srivastava, M.B.: Power management in energy harvesting sensor networks. ACM Trans. Embed. Comput. Syst. (2007). doi:10.​1145/​1274858.​1274870
50.
51.
Zurück zum Zitat Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRef Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRef
52.
Zurück zum Zitat Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002) Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)
53.
Zurück zum Zitat Lamport, L., Matthews, J., Tuttle, M.R., Yu, Y.: Specifying and verifying systems with TLA+. In: Muller, G., Jul, E. (eds.) ACM SIGOPS European Workshop, pp. 45–48. ACM (2002) Lamport, L., Matthews, J., Tuttle, M.R., Yu, Y.: Specifying and verifying systems with TLA+. In: Muller, G., Jul, E. (eds.) ACM SIGOPS European Workshop, pp. 45–48. ACM (2002)
54.
Zurück zum Zitat Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems—Safety. Springer, New York (1995)CrossRefMATH Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems—Safety. Springer, New York (1995)CrossRefMATH
55.
Zurück zum Zitat Méry, D.: A proof system to derive eventually properties under justice hypothesis. In: Gruska, J., Rovan, v, Wiedermann, J. (eds.) Mathematical Foundations of Computer Science 1986, Bratislava, Czechoslovakia, August 25–29, 1996, Proceedings, Lecture Notes in Computer Science, vol. 233, pp. 536–544. Springer (1986). doi:10.1007/BFb0016280 Méry, D.: A proof system to derive eventually properties under justice hypothesis. In: Gruska, J., Rovan, v, Wiedermann, J. (eds.) Mathematical Foundations of Computer Science 1986, Bratislava, Czechoslovakia, August 25–29, 1996, Proceedings, Lecture Notes in Computer Science, vol. 233, pp. 536–544. Springer (1986). doi:10.​1007/​BFb0016280
56.
Zurück zum Zitat Méry, D.: Requirements for a temporal B : Assigning Temporal Meaning to Abstract Machines ... and to Abstract Systems. In: Galloway, A., Taguchi, K. (eds.) IFM’99 Integrated Formal Methods 1999, Workshop on Computing Science, New York (1999) Méry, D.: Requirements for a temporal B : Assigning Temporal Meaning to Abstract Machines ... and to Abstract Systems. In: Galloway, A., Taguchi, K. (eds.) IFM’99 Integrated Formal Methods 1999, Workshop on Computing Science, New York (1999)
57.
Zurück zum Zitat Méry, D.: Refinement-based guidelines for algorithmic systems. Int. J. Softw. Inf. 3(2–3), 197–239 (2009) Méry, D.: Refinement-based guidelines for algorithmic systems. Int. J. Softw. Inf. 3(2–3), 197–239 (2009)
58.
Zurück zum Zitat Méry, D., Poppleton, M.: Formal modelling and verification of population protocols. In: Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10–14, 2013. Proceedings, pp. 208–222 (2013). doi:10.1007/978-3-642-38613-8_15 Méry, D., Poppleton, M.: Formal modelling and verification of population protocols. In: Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10–14, 2013. Proceedings, pp. 208–222 (2013). doi:10.​1007/​978-3-642-38613-8_​15
59.
Zurück zum Zitat Olderog, E.R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM Trans. Program. Lang. Syst. 10(3), 420–455 (1988)CrossRef Olderog, E.R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM Trans. Program. Lang. Syst. 10(3), 420–455 (1988)CrossRef
60.
Zurück zum Zitat Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982)CrossRefMATH Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982)CrossRefMATH
61.
Zurück zum Zitat Park, D.: A predicate transformer for weak fair iteration. In: Proceedings of 6th IBM Symposium on Mathematical Foundations in Computer Science, pp. 257–275. IBM, Hakone (1981) Park, D.: A predicate transformer for weak fair iteration. In: Proceedings of 6th IBM Symposium on Mathematical Foundations in Computer Science, pp. 257–275. IBM, Hakone (1981)
62.
Zurück zum Zitat Picco, G.: Software engineering and wireless sensor networks: happy marriage or consensual divorce. In: FoSER 2010 (2010) Picco, G.: Software engineering and wireless sensor networks: happy marriage or consensual divorce. In: FoSER 2010 (2010)
63.
Zurück zum Zitat Rajagopalan, R., Varshney, P.K.: Data-aggregation techniques in sensor networks: a survey. IEEE Commun. Surv. Tutor. 8(1–4), 48–63 (2006)CrossRef Rajagopalan, R., Varshney, P.K.: Data-aggregation techniques in sensor networks: a survey. IEEE Commun. Surv. Tutor. 8(1–4), 48–63 (2006)CrossRef
64.
Zurück zum Zitat Schneider, S.A., Treharne, H., Wehrheim, H., Williams, D.M.: Managing LTL properties in event-b refinement. In: Albert, E., Sekerinski, E. (eds.) Integrated Formal Methods—11th International Conference, IFM 2014, Bertinoro, Italy, September 9–11, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8739, pp. 221–237. Springer (2014). doi:10.1007/978-3-319-10181-1 Schneider, S.A., Treharne, H., Wehrheim, H., Williams, D.M.: Managing LTL properties in event-b refinement. In: Albert, E., Sekerinski, E. (eds.) Integrated Formal Methods—11th International Conference, IFM 2014, Bertinoro, Italy, September 9–11, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8739, pp. 221–237. Springer (2014). doi:10.​1007/​978-3-319-10181-1
65.
Zurück zum Zitat Spirakis, P.: Population protocols and related models. In: Theoretical Aspects of Distributed Computing in Sensor Networks Monographs in Theoretical Computer Science. An EATCS Series 2011, pp. 109–159. Springer (2011) Spirakis, P.: Population protocols and related models. In: Theoretical Aspects of Distributed Computing in Sensor Networks Monographs in Theoretical Computer Science. An EATCS Series 2011, pp. 109–159. Springer (2011)
66.
Zurück zum Zitat Stavvides, A., Srivastava, M., Girod, L., Estrin, D.: Wireless Sensor Networks. Springer, New York (2004) Stavvides, A., Srivastava, M., Girod, L., Estrin, D.: Wireless Sensor Networks. Springer, New York (2004)
Metadaten
Titel
Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols
verfasst von
Dominique Méry
Michael Poppleton
Publikationsdatum
29.12.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 4/2017
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-015-0504-y

Weitere Artikel der Ausgabe 4/2017

Software and Systems Modeling 4/2017 Zur Ausgabe