Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 2/2019

07-03-2018 | Original Article

Verification of asynchronous systems with an unspecified component

Authors: Rosa Abbasi, Fatemeh Ghassemi, Ramtin Khosravi

Published in: Acta Informatica | Issue 2/2019

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.
previous article Negotiation as concurrency primitive

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Appendix
Available only for authorised users
Footnotes
1
Scala programming language supports actor-models http://​www.​scala-lang.​org.
 
3
wiki.ros.org/Robots/Husky.
 
4
wiki.ros.org/Robots/Turtlebot.
 
Literature
1.
2.
Agha, G.A.: Actors: a model of concurrent computation in distributed systems. Tech. rep., DTIC Document (1985)
3.
Agha, G.A.: The structure and semantics of actor languages. In: Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems), pp. 1–59. Springer, Berlin (1990)
4.
5.
Almonaies, A.A., Cordy, J.R., Dean, T.R.: Legacy system evolution towards service-oriented architecture. In: International Workshop on SOA Migration and Evolution, pp. 53–62 (2010)
6.
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)MATHCrossRef
7.
Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: International Conference on Computer Aided Verification, pp. 548–562. Springer, Berlin (2005)
8.
Andersen, H.R., Stirling, C., Winskel, G.: A compositional proof system for the modal mu-calculus. In: Ninth Annual Symposium on Logic in Computer Science, pp. 144–153. IEEE Computer Society (1994)
9.
10.
Asaadi, H.R., Khosravi, R., Mousavi, M., Noroozi, N.: Towards model-based testing of electronic funds transfer systems. In: International Conference on Fundamentals of Software Engineering, pp. 253–267. Springer, Berlin (2011)
11.
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
12.
13.
Bloom, B., Fokkink, W., Van Glabbeek, R.J.: Precongruence formats for decorated trace semantics. ACM Trans. Comput. Log. 5(1), 26–78 (2004)MathSciNetMATHCrossRef
14.
Bobaru, M.G., Pasareanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: International Conference on Computer Aided Verification, pp. 135–148. Springer, Berlin (2008)
15.
Boreale, M., De Nicola, R., Pugliese, R.: Trace and testing equivalence on asynchronous processes. Inf. Comput. 172(2), 139–164 (2002)MathSciNetMATHCrossRef
16.
Brookes, S.D., Rounds, W.C.: Behavioural equivalence relations induced by programming logics. In: International Colloquium on Automata, Languages, and Programming, pp. 97–108. Springer, Berlin (1983)
17.
Canfora, G., Fasolino, A.R., Frattolillo, G., Tramontana, P.: A wrapping approach for migrating legacy system interactive functionalities to service oriented architectures. J. Syst. Softw. 81(4), 463–480 (2008)CrossRef
18.
Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, Berlin (2009)MATH
19.
Chaki, S., Strichman, O.: Optimized l*-based assume-guarantee reasoning. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 276–291. Springer, Berlin (2007)
20.
Cheung, S.C., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Trans. Softw. Eng. Methodol. 8(1), 49–78 (1999)CrossRef
21.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)MATH
22.
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Proceedings of 4th Annual Symposium on Logic in Computer Science, pp. 353–362. IEEE (1989)
23.
Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 7 (2008)CrossRef
24.
Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 331–346. Springer, Berlin (2003)
25.
Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers. IEICE Trans. Inf. Syst. 80(3), 315–325 (1997)
26.
Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Logic Synthesis for Asynchronous Controllers and Interfaces, vol. 8. Springer, Berlin (2012)MATH
27.
Dai, G., Bai, X., Zhao, C.: A framework for model checking web service compositions based on bpel4ws. In: International Conference on e-Business Engineering, pp. 165–172. IEEE (2007)
28.
29.
Fabian, M., Lennartson, B.: On non-deterministic supervisory control. In: Proceedings of the 35th IEEE Conference on Decision and Control, vol. 2, pp. 2213–2218. IEEE (1996)
30.
Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: European Symposium on Programming, pp. 173–188. Springer, Berlin (2007)
31.
Fokkink, W., Van Glabbeek, R., De Wind, P.: Compositionality of hennessy-milner logic by structural operational semantics. Theor. Comput. Sci. 354(3), 421–440 (2006)MathSciNetMATHCrossRef
32.
Foster, H., Uchitel, S., Magee, J., Kramer, J.: Ws-engineer: a model-based approach to engineering web service compositions and choreography. In: Test and Analysis of Web Services, pp. 87–119. Springer, Berlin (2007)
33.
Gao, C., Liu, R., Song, Y., Chen, H.: A model checking tool embedded into services composition environment. In: International Conference on Grid and Cooperative Computing, pp. 355–362. IEEE (2006)
34.
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Autom. Softw. Eng. 12(3), 297–320 (2005)CrossRef
35.
Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: International Joint Conference on Automated Reasoning, pp. 483–497. Springer, Berlin (2006)
36.
Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)MATHCrossRef
37.
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)CrossRef
38.
Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. In: International Conference on Computer Aided Verification, pp. 420–432. Springer, Berlin (2007)
39.
40.
Hewitt, C.: Orgs for scalable, robust, privacy-friendly client cloud computing. IEEE Internet Comput. 12(5), 96 (2008)CrossRef
41.
42.
43.
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)MATHCrossRef
44.
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Softw. Syst. Model. 6(1), 39–58 (2007)CrossRef
45.
Johnsen, E.B., Owe, O., Yu, I.C.: Creol: a type-safe object-oriented model for distributed concurrent systems. Theoret. Comput. Sci. 365(1), 23–66 (2006)MathSciNetMATHCrossRef
46.
Jones, C.B.: Specification and design of (parallel) programs. IFIP Congress 83, 321–332 (1983)
47.
Karmani, R.K., Shali, A., Agha, G.A.: Actor frameworks for the JVM platform: a comparative analysis. In: Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, pp. 11–20. ACM (2009)
48.
Kupferman, O., Lampert, R.: On the construction of fine automata for safety properties. In: Automated Technology for Verification and Analysis, 4th International Symposium. Lecture Notes in Computer Science, vol. 4218, pp. 110–124. Springer, Berlin (2006)
49.
Larsen, K.G.: Context-dependent bisimulation between processes (1986)
50.
51.
Lewis, G., Morris, E., Smith, D., O’Brien, L.: Service-oriented migration and reuse technique (smart). In: 13th IEEE International Workshop on Software Technology and Engineering Practice, pp. 222–229. IEEE (2005)
52.
Linthicum, D.S.: Enterprise Application Integration. Addison-Wesley, Reading (2000)
53.
Markovski, J.: A process-theoretic approach to supervisory coordination under partial observation. Sci. Comput. Program. 115, 127–145 (2016)CrossRef
54.
Nam, W., Alur, R.: Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: International Symposium on Automated Technology for Verification and Analysis, pp. 170–185. Springer, Berlin (2006)
55.
Nam, W., Madhusudan, P., Alur, R.: Automatic symbolic compositional verification by learning assumptions. Formal Methods Syst. Des. 32(3), 207–234 (2008)MATHCrossRef
56.
57.
Overkamp, A.: Supervisory control using failure semantics and partial specifications. IEEE Trans. Autom. Control 42(4), 498–510 (1997)MathSciNetMATHCrossRef
58.
Parveen, T., Tilley, S.: A research agenda for testing soa-based systems. In: 2nd Annual IEEE Systems Conference, pp. 1–6. IEEE (2008)
59.
Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175–205 (2008)MATHCrossRef
60.
Pena, J.M., Oliveira, A.L.: A new algorithm for exact reduction of incompletely specified finite state machines. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18(11), 1619–1632 (1999)CrossRef
61.
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, pp. 123–144. Springer, Berlin (1985)
62.
Raclet, J.B.: Residual for component specifications. Electron. Notes Theor. Comput. Sci. 215, 93–110 (2008)CrossRef
63.
Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. In: Analysis and Optimization of Systems, pp. 475–498. Springer, Berlin (1984)
64.
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetMATHCrossRef
65.
Sen, K.: Concolic testing and constraint satisfaction. In: International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science, vol. 6695, pp. 3–4. Springer, Berlin (2011)
66.
Sirjani, M.: Rebeca: Theory, Applications, and Tools, pp. 102–126. Springer, Berlin (2007)
67.
Sirjani, M., Movaghar, A., Shali, A., De Boer, F.S.: Modeling and verification of reactive systems using rebeca. Fundam. Informaticae 63(4), 385–410 (2004)MathSciNetMATH
68.
Szyperski, C.: Component Software: Beyond Object-oriented Programming, 2nd edn. Addison-Wesley Longman Publishing Co., Inc, Boston (2002)MATH
69.
Thati, P., Ziaei, R., Agha, G.: A theory of may testing for actors. In: IFIP TC6/WG6.1 Fifth International Conference on Formal Methods for Open Object-Based Distributed Systems. IFIP Conference Proceedings, vol. 209, pp. 147–162. Kluwer, Dordrecht (2002)
70.
Van Hulst, A.C., Reniers, M.A., Fokkink, W.J.: Maximal synthesis for hennessy-milner logic. ACM Trans. Embed. Comput. Syst. 14(1), 10 (2015)CrossRef
71.
Wan, K.M., Lei, P., Chatwin, C., Young, R.: Service-oriented architecture. Encycl. E-Commer. E-Gov. Mob. Commer. 160(1), 998–1002 (2006)
72.
Zakeriyan, A., Khamespanah, E., Sirjani, M., Khosravi, R.: Jacco: more efficient model checking toolset for java actor programs. In: Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, pp. 37–44. ACM (2015)
73.
Zheng, Y., Zhou, J., Krause, P.: A model checking based test case generation framework forweb services. In: International Conference on Information Technology, pp. 715–722. IEEE (2007)
Metadata
Title
Verification of asynchronous systems with an unspecified component
Authors
Rosa Abbasi
Fatemeh Ghassemi
Ramtin Khosravi
Publication date
07-03-2018
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 2/2019
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-018-0317-x

Premium Partner

    Image Credits