Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1109/ASE.2003.1240300acmconferencesArticle/Chapter ViewAbstractPublication PagesaseConference Proceedingsconference-collections
Article

Automated environment generation for software model checking

Published: 06 October 2003 Publication History

Abstract

A key problem in model checking open systems is environment modeling (i.e., representing the behavior of the execution context of the system under analysis). Software systems are fundamentally open since their behavior is dependent on patterns of invocation of system components and values defined outside the system but referenced within the system. Whether reasoning about the behavior of whole programs or about program components, an abstract model of the environment can be essential in enabling sufficiently precise yet tractable verification.
In this paper, we describe an approach to generating environments of Java program fragments. This approach integrates formally specified assumptions about environment behavior with sound abstractions of environment implementations to form a model of the environment. The approach is implemented in the Bandera Environment Generator (BEG) which we describe along with our experience using BEG to reason about properties of several non-trivial concurrent Java programs.

References

[1]
A. Aho, R. Sethi, and J. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley, 1985.
[2]
R. Alur, L. de Alfaro, R. Grosu, T. A. Henzinger, M. Kang, C. M. Kirsch, R. Majumdar, F. Mang, and B.-Y. Wang. jMocha: A model-checking tool that exploits design structure. In Proceedings of the 23rd Annual IEEE/ACM International Conference on Software Engineering, pages pp. 835-836. IEEE Computer Society Press, 2001.
[3]
G. S. Avrunin, J. C. Corbett, and L. Dillon. Analyzing partially-implemented real-time systems. In Proceedings of the 19th International Conference on Software Engineering, pages 228-238, 1997.
[4]
T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the ACM SIGPLAN '01 Conference on Programming Language Design and Implementation (PLDI-01), volume 36.5 of ACM SIGPLAN Notices, pages 203-213. ACM Press, June 20-22 2001.
[5]
J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference (LNCS 2619), Apr. 2003.
[6]
C. Colby, P. Godefroid, and L. J. Jagadeesan. Automatically closing open reactive programs. In SIGPLAN Conference on Programming Language Design and Implementation, pages 345-357, 1998.
[7]
J. C. Corbett. Constructing compact models of concurrent Java programs. In M. Young, editor, Proceedings of the 1998 International Symposium on Software Testing and Analysis (ISSTA). ACM Press, March 1998.
[8]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera : Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering, June 2000.
[9]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: The Bandera specification language. International Journal on Software Tools for Technology Transfer, 4(1):34-56, 2002.
[10]
M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of the 23rd International Conference on Software Engineering, May 2001.
[11]
M. B. Dwyer and C. S. Pasareanu. Filter-based model checking of partial systems. In Proceedings of the Sixth ACM SIGSOFT Symposium on Foundations of Software Engineering, Nov. 1998.
[12]
M. B. Dwyer and V. Wallentine. A framework for parallel adaptive grid simulations. Concurrency - Practice and Experience, 9(11):1293-1310, 1997.
[13]
C. Flanagan and S. Qadeer. Thread modular model checking. In Model Checking Software (LNCS 2648), May 2003.
[14]
D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In Proceedings of the 17th IEEE Conference on Automated Software Engineering, May 2002.
[15]
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pages 58-70, Jan. 2002.
[16]
G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-294, May 1997.
[17]
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.
[18]
R. Milner. Communication and Concurrecy. Prentice Hall, 1989.
[19]
J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger. Verification of time partitioning in the DEOS real-time scheduling kernel. In Proceedings of the 22nd International Conference on Software Engineering, June 2000.
[20]
C. S. Pasareanu. DEOS kernel: Environment modeling using LTL assumptions. Technical Report Technical Report NASA-ARC-IC-2000-196, NASA Ames, 2000.
[21]
C. S. Pasareanu. Abstraction and Modular Reasoning for the Verification of Software. PhD thesis, Kansas State University, 2001.
[22]
C. S. Pasareanu, M. B. Dwyer, and M. Huth. Assume-guarantee model checking of software : A comparative case study. In Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680), Sept. 1999.
[23]
S. D. Stoller. Domain partitioning for open reactive systems. In Proceedings of the international symposium on Software testing and analysis, pages 44-54. ACM Press, 2002.
[24]
O. Tkachuk. Adapting side effects analysis for modular program model checking. Master's thesis, Kansas State University, 2003.
[25]
O. Tkachuk, G. Brat, and W. Visser. Using code level model checking to discover automation surprises. In Proceedings of the 2002 Digital Avionics Systems Conference, Oct. 2002.
[26]
O. Tkachuk and M. B. Dwyer. Adapting side effects analysis for modular program model checking. In Proceedings of the Fourth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, Sept. 2003.
[27]
R. Valle-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Java optimization framework. In Proceedings of CASCON'99, Nov. 1999.
[28]
W. Visser, G. Brat, K. Havelund, and S. Park. Model checking programs. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering, Sept. 2000.

Cited By

View all
  • (2023)RoboWorld: Verification of Robotic Systems with Environment in the LoopFormal Aspects of Computing10.1145/362556335:4(1-46)Online publication date: 27-Sep-2023
  • (2020)Modular deployment of UML models for V&V activities and embedded executionProceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3417990.3419227(1-10)Online publication date: 16-Oct-2020
  • (2018)Stateless techniques for generating global and local test oracles for message-passing concurrent programsJournal of Systems and Software10.1016/j.jss.2017.11.026136:C(237-265)Online publication date: 1-Feb-2018
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
ASE'03: Proceedings of the 18th IEEE International Conference on Automated Software Engineering
October 2003
380 pages
ISBN:0769520359

Sponsors

Publisher

IEEE Press

Publication History

Published: 06 October 2003

Check for updates

Qualifiers

  • Article

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2023)RoboWorld: Verification of Robotic Systems with Environment in the LoopFormal Aspects of Computing10.1145/362556335:4(1-46)Online publication date: 27-Sep-2023
  • (2020)Modular deployment of UML models for V&V activities and embedded executionProceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings10.1145/3417990.3419227(1-10)Online publication date: 16-Oct-2020
  • (2018)Stateless techniques for generating global and local test oracles for message-passing concurrent programsJournal of Systems and Software10.1016/j.jss.2017.11.026136:C(237-265)Online publication date: 1-Feb-2018
  • (2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
  • (2017)Constraint-based test generation for automotive operating systemsSoftware and Systems Modeling (SoSyM)10.1007/s10270-014-0449-616:1(7-24)Online publication date: 1-Feb-2017
  • (2017)Environment-driven reachability for timed systemsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0401-219:2(229-245)Online publication date: 1-Apr-2017
  • (2016)Automatic model generation from documentation for Java API functionsProceedings of the 38th International Conference on Software Engineering10.1145/2884781.2884881(380-391)Online publication date: 14-May-2016
  • (2015)Environment modeling in model-based testingProceedings of the 19th International Conference on Evaluation and Assessment in Software Engineering10.1145/2745802.2745830(1-6)Online publication date: 27-Apr-2015
  • (2015)Automated system-level safety testing using constraint patterns for automotive operating systemsProceedings of the 30th Annual ACM Symposium on Applied Computing10.1145/2695664.2695935(1815-1822)Online publication date: 13-Apr-2015
  • (2015)Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generationScience of Computer Programming10.1016/j.scico.2014.10.006103:C(51-70)Online publication date: 1-Jun-2015
  • Show More Cited By

View Options

View options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media