nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them

verfasst von : Tam Thi Thanh Nguyen, Kazuhiro Ogata

Erschienen in: Structured Object-Oriented Formal Language and Method

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

The MCS list-based queuing lock (MCS) is a mutual exclusion protocol whose variants have been used in Java virtual machines. MCS is specified as a state machine in Maude, a rewriting logic-based computer language and system. We have developed a tool (called SMGA) that tales a finite computation generated from a state machine and displays its graphical animations. MCS is used to describe how such graphical animations help human beings perceive characteristics of the state machine of MCS. Such characteristics can be confirmed by Maude model checking facilities. The characteristics graphically perceived and confirmed by model checking could be used as lemmas to theorem prove that MCS enjoys some desired properties. SMGA can also display graphical animations of counterexamples presented by the Maude LTL model checker.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Nächstes Kapitel An Investigation of Integrating a GUI-Aided Approach and a Specification-Based Testing

If you find a good abstraction that converts an infinite-state system to a finite-state one and preserves the negation of a property concerned, the infinite-state system can be formally verified by model checking the finite-state one [1, 2], although you need to prove the preservation of the negated property by the abstraction.

https://www.podc.org/dijkstra/2006-dijkstra-prize/.

Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16, 1512–1542 (1994)CrossRef

Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. Theor. Comput. Sci. 403, 239–264 (2008)MathSciNetCrossRef

Nguyen, T.T.T., Ogata, K.: Graphical animations of state machines. Submitted for Publication (2017). https://tamntt.bitbucket.io/Research/Paper/smga.pdf

Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9, 21–65 (1991)CrossRef

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude – A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1CrossRefMATH

Liard, J.: Draw SVG Website (2015). http://www.drawsvg.org/

Nguyen, T.T.T., Ogata, K.: A way to comprehend counterexamples generated by Maude LTL model checker. Submitted for Publication (2017)

Wang, F.: Automatic verification of pointer data-structure systems for all numbers of processes. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 328–347. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_20CrossRef

Wang, F., Schmidt, K.: Symmetric symbolic safety-analysis of concurrent software with pointer data structures. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 50–64. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36135-9_4CrossRef

10.

Ogata, K., Futatsugi, K.: Formal verification of the MCS list-based queuing lock. In: Thiagarajan, P.S., Yap, R. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 281–293. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46674-6_24CrossRef

11.

Schellhorn, G., Travkin, O., Wehrheim, H.: Towards a thread-local proof technique for starvation freedom. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 193–209. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_13CrossRef

12.

Hallerstede, S., Leuschel, M., Plagge, D.: Refinement-animation for event-B – towards a method of validation. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 287–301. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_22CrossRef

13.

Hallerstede, S., Leuschel, M., Plagge, D.: Validation of formal models by refinement animation. Sci. Comput. Program. 78, 272–292 (2013)CrossRef

14.

Liu, S.: Validating formal specifications using testing-based specification animation. In: FormaliSE@ICSE 2016, pp. 29–35 (2016)

15.

Li, M., Liu, S.: Integrating animation-based inspection into formal design specification construction for reliable software systems. IEEE Trans. Reliabil. 65, 88–106 (2016)CrossRef

16.

Liang, H., Dong, J.S., Sun, J., Wong, W.E.: Software monitoring through formal specification animation. ISSE 5, 231–241 (2009)

Titel: Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them
verfasst von: Tam Thi Thanh Nguyen
Kazuhiro Ogata
Verlag: Springer International Publishing
Buch: Structured Object-Oriented Formal Language and Method
Print ISBN: 978-3-319-90103-9

Electronic ISBN: 978-3-319-90104-6

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-90104-6_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"