More Web Proxy on the site http://driver.im/

poster

Integrating model verification and self-adaptation

Authors:

Rafael V. Borges,

Artur d'Avila Garcez,

Luis C. LambAuthors Info & Claims

ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

Pages 317 - 320

https://doi.org/10.1145/1858996.1859060

Published: 20 September 2010 Publication History

Abstract

In software development, formal verification plays an important role in improving the quality and safety of products and processes. Model checking is a successful approach to verification, used both in academic research and industrial applications. One important improvement regarding utilization of model checking is the development of automated processes to evolve models according to information obtained from verification. In this paper, we propose a new framework that make use of artificial intelligence and machine learning to generate and evolve models from partial descriptions and examples created by the model checking process. This was implemented as a tool that is integrated with a model checker. Our work extends model checking to be applicable when initial description of a system is not available, through observation of actual behaviour of this system. The framework is capable of integrated verification and evolution of abstract models, but also of reengineering partial models of a system.

References

[1]

}}D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel. Learning operational requirements from goal models. In ICSE '09: Intl. Conf. Softw. Engineering, pages 265--275. IEEE, 2009.

Digital Library

[2]

}}R. Andrews, J. Diederich, and A. B. Tickle. A survey and critique of techniques for extracting rules from trained artificial neural networks. Knowledge-based Systems, 8(6):373--389, 1995.

Digital Library

[3]

}}D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast: Applications to software engineering. International Journal on Software Tools for Technology Transfer (STTT), 9(5-6):505--525, 2007.

Digital Library

[4]

}}M. G. Bobaru, C. S. Pasareanu, and D. Giannakopoulou. Automated assume-guarantee reasoning by abstraction refinement. In CAV, pages 135--148, 2008.

Digital Library

[5]

}}A. Browne and R. Sun. Connectionist inference models. Neural Networks, 14(10):1331--1355, 2001.

Digital Library

[6]

}}A. Cimatti, M. Pistore, M. Roveri, and R. Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In VMCAI'02, volume 2294 of LNCS. Springer, 2002.

Digital Library

[7]

}}E. Clarke, E. Emerson, and J. Sifakis. Model checking: algorithmic verification and debugging. Commun. ACM, 52(11):74--84, 2009.

Digital Library

[8]

}}E. Clarke, O Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752--794, 2003.

Digital Library

[9]

}}A. S. d'Avila Garcez, K. Broda, and D. M. Gabbay. Neural-Symbolic Learning Systems: Foundations and Applications. Perspectives in Neural Computing. Springer-Verlag, 2002.

Digital Library

[10]

}}A. S. d'Avila Garcez, L. C. Lamb, and D. M. Gabbay. Neural-Symbolic Cognitive Reasoning. Cognitive Technologies. Springer, 2009.

Digital Library

[11]

}}A. S. d'Avila Garcez, A. Russo, B. Nuseibeh, and J. Kramer. An analysis-revision cycle to evolve requirements specifications. In ASE, pages 354--358, 2001.

Digital Library

[12]

}}A. S. d'Avila Garcez and G. Zaverucha. The connectionist inductive learning and logic programming system. Applied Intelligence, 11(1):59--77, 1999.

Digital Library

[13]

}}J. Deshmukh, E. Emerson, and S. Sankaranarayanan. Symbolic deadlock analysis in concurrent libraries and their clients. In ASE, pages 480--491, 2009.

Digital Library

[14]

}}S. Dobson, S. Denazis, A. Fernández, D. Gaïti, Gelenbe, Massacci, P. Nixon, F. Saffre, N. Schmidt, and F. Zambonelli. A survey of autonomic communications. ACM TAAS, 1(2):223--259, 2006.

Digital Library

[15]

}}S. Dobson, R. Sterritt, P. Nixon, and M. Hinchey. Fulfilling the vision of autonomic computing. IEEE Computer, 43(1):35--41, 2010.

Digital Library

[16]

}}M. Fisher, D. Gabbay, and L. Vila, editors. Handbook of temporal reasoning in artificial intelligence. Elsevier, 2005.

Digital Library

[17]

}}S. Haykin. Neural Networks: A Compreensive Foundation. Prentice Hall, 2nd edition, 1999.

Digital Library

[18]

}}P. Hitzler, S. Hölldobler, and A. K. Seda. Logic programs and connectionist networks. J. Applied Logic, 2(3):245--272, 2004.

[19]

}}L. C. Lamb, R. V. Borges, and A. S. d'Avila Garcez. A connectionist cognitive model for temporal synchronization and learning. In Proc. of 22nd AAAI Conf. on Artificial Intelligence, pages 827--832, 2007.

Digital Library

[20]

}}D. L. Parnas. Really rethinking 'formal methods'. IEEE Computer, 43(1):28--34, 2010.

Digital Library

[21]

}}D. Peled, M. Y. Vardi, and M. Yannakakis. Black box checking. J. of Automata Languages and Combinatorics, 7(2):225--246, 2001.

Digital Library

[22]

}}A. Pnueli. The temporal logic of programs. In FOCS '77: Proc. 18th IEEE Symp.on Foundations of Computer Science, pages 46--67. IEEE Computer Society, 1977.

Digital Library

[23]

}}L. G. Valiant. Three problems in computer science. Journal of ACM, 50(1):96--99, 2003.

Digital Library

Cited By

Zhu WWu HDeng M(2019)LTL Model Checking Based on Binary Classification of Machine LearningIEEE Access10.1109/ACCESS.2019.29427627(135703-135719)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2942762
Daun MWeyer TPohl K(2019)Improving manual reviews in function-centered engineering of embedded systems using a dedicated review modelSoftware & Systems Modeling10.1007/s10270-019-00723-2Online publication date: 2-Feb-2019
https://doi.org/10.1007/s10270-019-00723-2
Brings J(2017)Verifying Cyber-Physical System Behavior in the Context of Cyber-Physical System-Networks2017 IEEE 25th International Requirements Engineering Conference (RE)10.1109/RE.2017.45(556-561)Online publication date: Sep-2017
https://doi.org/10.1109/RE.2017.45
Show More Cited By

Index Terms

Integrating model verification and self-adaptation

Recommendations

Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

September 2010

534 pages

ISBN:9781450301169

DOI:10.1145/1858996

General Chair:
Charles Pecheur
Université catholique de Louvain, Belgium
,
Program Chairs:
Jamie Andrews
University of Western Ontario, Canada
,
Elisabetta Di Nitto
Politecnico di Milano, Italy

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Poster

Conference

ASE10

Sponsor:

ASE10: IEEE/ACM International Conference on Automated Software Engineering

September 20 - 24, 2010

Antwerp, Belgium

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
308
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhu WWu HDeng M(2019)LTL Model Checking Based on Binary Classification of Machine LearningIEEE Access10.1109/ACCESS.2019.29427627(135703-135719)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2942762
Daun MWeyer TPohl K(2019)Improving manual reviews in function-centered engineering of embedded systems using a dedicated review modelSoftware & Systems Modeling10.1007/s10270-019-00723-2Online publication date: 2-Feb-2019
https://doi.org/10.1007/s10270-019-00723-2
Brings J(2017)Verifying Cyber-Physical System Behavior in the Context of Cyber-Physical System-Networks2017 IEEE 25th International Requirements Engineering Conference (RE)10.1109/RE.2017.45(556-561)Online publication date: Sep-2017
https://doi.org/10.1109/RE.2017.45
Daun MWeyer TPohl K(2015)Detecting and Correcting Outdated Requirements in Function-Centered Engineering of Embedded SystemsRequirements Engineering: Foundation for Software Quality10.1007/978-3-319-16101-3_5(65-80)Online publication date: 14-Mar-2015
https://doi.org/10.1007/978-3-319-16101-3_5
Yang WXu CLiu YCao CMa XLu JCrnkovic IChechik MGrünbacher P(2014)Verifying self-adaptive applications suffering uncertaintyProceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering10.1145/2642937.2642999(199-210)Online publication date: 15-Sep-2014
https://dl.acm.org/doi/10.1145/2642937.2642999
Weyns DIftikhar Mde la Iglesia DAhmad TDesai BVassev EMudur SDesai B(2012)A survey of formal methods in self-adaptive systemsProceedings of the Fifth International C* Conference on Computer Science and Software Engineering10.1145/2347583.2347592(67-79)Online publication date: 27-Jun-2012
https://dl.acm.org/doi/10.1145/2347583.2347592
Weyns DBodden EMusuvathi M(2012)Towards an integrated approach for validating qualities of self-adaptive systemsProceedings of the Ninth International Workshop on Dynamic Analysis10.1145/2338966.2336803(24-29)Online publication date: 15-Jul-2012
https://dl.acm.org/doi/10.1145/2338966.2336803

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents