article

Using source transformation to test and model check implicit-invocation systems

Authors:

Jeremy S. Bradbury,

James R. Cordy,

Juergen DingelAuthors Info & Claims

Science of Computer Programming, Volume 62, Issue 3

Pages 209 - 227

https://doi.org/10.1016/j.scico.2006.04.008

Published: 15 October 2006 Publication History

Abstract

In this paper we present a source transformation-based framework to support uniform testing and model checking of implicit-invocation software systems. The framework includes a new domain-specific programming language, the Implicit-Invocation Language (IIL), explicitly designed for directly expressing implicit-invocation software systems, and a set of formal rule-based source transformation tools that allow automatic generation of both executable and formal verification artifacts. We provide details of these transformation tools, evaluate the framework in practice, and discuss the benefits of formal automatic transformation in this context. Our approach is designed not only to advance the state-of-the-art in validating implicit-invocation systems, but also to further explore the use of automated source transformation as a uniform vehicle to assist in the implementation, validation and verification of programming languages and software systems in general.

References

[1]

{1} J. Corbett, M. Dwyer, J. Hatcliff et al., Bandera: Extracting finite-state models from Java source code, in: Proc. Int. Conf. on Software Engineering, 2000, pp. 439-458.]]

Digital Library

[2]

{2} H. Zhang, J.S. Bradbury, J.R. Cordy, J. Dingel, A transformational framework for testing and model checking implicit-invocation systems, in: Proc. Int. Work. on Distr. Event-Based Systems, DEBS'04, 2004, pp. 110-115.]]

[3]

{3} H. Zhang, J.S. Bradbury, J.R. Cordy, J. Dingel, Implementation and verification of implicit-invocation systems using source transformation, in: Proc. Int. Work. on Source Code Analysis and Manipulation, SCAM 2005, 2005, pp. 87-96.]]

Digital Library

[4]

{4} D. Garlan, S. Khersonsky, Model checking implicit-invocation systems, in: Proc. Int. Work. on Software Spec. and Design, 2000, pp. 23-30.]]

Digital Library

[5]

{5} D. Garlan, S. Khersonsky, J. Kim, Model checking publish-subscribe systems, in: Proc. Int. SPIN Work. on Model Checking of Software, 2003, pp. 166-180.]]

[6]

{6} J.S. Bradbury, J. Dingel, Evaluating and improving the automatic analysis of implicit invocation systems, in: Proc. ESEC/FSE 2003, 2003, pp. 78-87.]]

Digital Library

[7]

{7} K. McMillan, Getting started with SMV, Cadence Berkeley Laboratories.]]

[8]

{8} R. Holt, J. Cordy, The Turing Plus Report, CSRI, Univ. of Toronto.]]

[9]

{9} K. Sullivan, D. Notkin, Reconciling environment integration and software evolution, in: Proc. SIGSOFT '90 Symp. on Software Development Environments, 1990, pp. 22-23.]]

Digital Library

[10]

{10} R. Holt, J. Cordy, The turing programming language, Communications of the ACM 31 (12) (1988) 1410-1423.]]

Digital Library

[11]

{11} J. Cordy, TXL -- a language for programming language tools and applications, in: Proc. 4th Int. Workshop on Language Descriptions, Tools and Applications, Electronic Notes in Theoretical Computer Science 110 (2004) 3-31.]]

Digital Library

[12]

{12} J. Cordy, T. Dean, A. Malton, K. Schneider, Source transformation in software engineering using the TXL transformation system, Journal of Information and Software Technology 44 (13) (2002) 827-837.]]

[13]

{13} E. Visser, Stratego: A language for program transformation based on rewriting strategies, in: Proc. Rewriting Techniques and Applications (RTA01), Lecture Notes in Computer Science 2051 (2001) 357-361.]]

Digital Library

[14]

{14} M. van den Brand, P Klint et al., The ASF+SDF meta-environment: A component-based language development environment, in: Proc. 1st Int. Workshop on Language Descriptions, Tools and Applications, Electronic Notes in Theoretical Computer Science 44 (2).]]

[15]

{15} T. Parr, R. Quong, ANTLR: A predicated- LL(k) parser generator, Software-Practice and Experience 25 (7) (1995) 789-810.]]

Digital Library

[16]

{16} K. Havelund, G. Rosu, Synthesizing monitors for safety properties, in: Proc. Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, 2002, pp. 342-356.]]

Digital Library

[17]

{17} R.A. DeMillo, R.J. Lipton, F.G. Sayward, Program mutation: A new approach to program testing, in: Infotech State of the Art Report, Software Testing, Volume 2: Invited Papers, Infotech International, 1979, pp. 107-126.]]

[18]

{18} J.S. Bradbury, J.R. Cordy, J. Dingel, An empirical framework for comparing effectiveness of testing and property-based formal analysis, in: International ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE 2005, 2005, pp. 1-4.]]

Digital Library

[19]

{19} D. Luckham, J. Vera, An event-based architecture definition language, IEEE Transactions on Software Engineering 21 (9)(1995) 717-734.]]

Digital Library

[20]

{20} J. Patterson, An object-oriented event calculus, Tech. Rep. TR02-08, Iowa State University, 2002.]]

[21]

{21} mdthread.org, Message-driven thread API for the Java programming language, Web page: http://www.mdthread.org.]]

[22]

{22} B. Segall, D. Arnold, Elvin has left the building:A publish/subscribe notification service with quenching, in: Proc. AUUG'97, 1997.]]

[23]

{23} A. Carzaniga, D. Rosenblum, A. Wolf, Design and evaluation of a wide-area event notification service, ACM Transactions on Computer Systems 19 (3) (2001) 332-383. URL: http://www.cs.colorado.edu/~carzanig/papers/index.html.]]

Digital Library

[24]

{24} S.D. Stoller, Testing concurrent java programs using randomized scheduling, in: Second Workshop on Runtime Verification, RV'02, 2002.]]

[25]

{25} Robby, M.B. Dwyer, J. Hatcliff, Bogor: An extensible and highly-modular software model checking framework, in: ESEC/FSE-II: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ACM Press, New York, NY, USA, 2003, pp. 267-276.]]

Digital Library

[26]

{26} T. Cassidy, J. Cordy, T. Dean, J. Dingel, Source transformation for concurrency analysis, in: Proc. 5th Int. Workshop on Language Descriptions, Tools and Applications, 2005, pp. 26-43.]]

[27]

{27} S. Qadeer, D. Wu, KISS: Keep it simple and sequential, in: Proc. PLDI 2004, ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, 2004, pp. 14-24.]]

Digital Library

Cited By

Cai LBradbury JDingel J(2007)Verifying distributed, event-based middleware applications using domain-specific software model checkingProceedings of the 9th IFIP WG 6.1 international conference on Formal methods for open object-based distributed systems10.5555/1772150.1772155(44-58)Online publication date: 6-Jun-2007
https://dl.acm.org/doi/10.5555/1772150.1772155

Recommendations

Source transformation, analysis and generation in TXL
PEPM '06: Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation

The TXL transformation framework has been widely used in practical source transformation tasks in industry and academia for many years. At the core of the framework is the TXL language, a functional programming language specifically designed for ...
Testing domain-specific languages
OOPSLA '11: Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion

The Spoofax testing language provides a new approach to testing domain-specific languages as they are developed. It allows test cases to be written using fragments of the language under test, providing full IDE support for writing test cases and ...
Integrated language definition testing: enabling test-driven language development
OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications

The reliability of compilers, interpreters, and development environments for programming languages is essential for effective software development and maintenance. They are often tested only as an afterthought. Languages with a smaller scope, such as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Science of Computer Programming

Science of Computer Programming Volume 62, Issue 3

Special issue on source code analysis and manipulation (SCAM 2005)

15 October 2006

113 pages

ISSN:0167-6423

Issue’s Table of Contents

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 15 October 2006

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cai LBradbury JDingel J(2007)Verifying distributed, event-based middleware applications using domain-specific software model checkingProceedings of the 9th IFIP WG 6.1 international conference on Formal methods for open object-based distributed systems10.5555/1772150.1772155(44-58)Online publication date: 6-Jun-2007
https://dl.acm.org/doi/10.5555/1772150.1772155

View Options

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

Media

Figures

Other

Tables

View Issue’s Table of Contents