Patterns in property specifications for finite-state verification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Patterns in property specifications for finite-state verification

Full text

Pdf (1.20 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 21st international conference on Software engineering table of contents

Los Angeles, California, United States

Pages: 411 - 420

Year of Publication: 1999

ISBN:1-58113-074-0

Authors

Matthew B. Dwyer	Kansas State University, Department of Computing and Information Sciences, Manhattan, KS
George S. Avrunin	University of Massachusetts, Department of Mathematics and Statistics, Amherst, MA
James C. Corbett	University of Hawai'i, Department of Information and Computer Science, Honolulu, HI

Sponsors

IEEE-CS : Computer Society
IEEE-CS\TCSE : TC on Software Engineering
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGSOFT: ACM Special Interest Group on Software Engineering
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 43, Downloads (12 Months): 176, Citation Count: 86

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/302405.302672 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
	2	K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
	3	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	4	Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
	5	James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
	6	Robert Darimont , Axel van Lamsweerde, Formal refinement patterns for goal-driven requirements elaboration, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.179-190, October 16-18, 1996, San Francisco, California, United States
	7	L. K. Dillon , G. Kutty , L. E. Moser , P. M. Melliar-Smith , Y. S. Ramakrishna, A graphical interval logic for specifying concurrent systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.131-165, April 1994 [doi>10.1145/192218.192226]
	8	Dover, G. Avrunin, and J. Corbett. A System of Specification Patterns. http: //uvw . cis . ksu. edu/ santos/spec-patterns, 1997.
	9	Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States [doi>10.1145/298595.298598]
	10	Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.62-75, Dec. 1994
	11	N. E. Fuchs 'and R. Schwitter. Attempt0 Controlled English (ACE). In CLAW 96, the First International Workshop on Controlled Language Applications, 1996.
	12	Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
	13	N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous programming language LUS- TRE. Proceedings of the IEEE, 79(9), Sept. 1991.
	14	Z. Har'El and R. P. Kurshan. Software for analytical devleopment of communication protocols. AT&T Technical Journal, 69(1):44-59, 1990.
	15	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
	16	Z Manna , Amir Pnueli, Tools and rules for the practicing verifier, Stanford University, Stanford, CA, 1990
	17	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	18	Philippe Massonet , Axel Van Lamsweerde, Analogical Reuse of Requirements Frameworks, Proceedings of the 3rd IEEE International Symposium on Requirements Engineering (RE'97), p.26, January 05-08, 1997
	19	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	20	Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
	21	Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
	22	David S. Rosenblum, Formal methods and testing: why the state-of-the art is not the state-of-the practice, ACM SIGSOFT Software Engineering Notes, v.21 n.4, p.64-66, July 1996 [doi>10.1145/232069.232086]

CITED BY 87

	Bin Chen , George S. Avrunin , Elizabeth A. Henneman , Lori A. Clarke , Leon J. Osterweil , Philip L. Henneman, Analyzing medical processes, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Gerard J. Holzmann, The logic of bugs, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
	Radu Mateescu , Mihaela Sighireanu, Efficient on-the-fly model-checking for regular alternation-free mu-calculus, Science of Computer Programming, v.46 n.3, p.255-281, March 2003
	James C. Corbett, Using shape analysis to reduce finite-state models of concurrent Java programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.51-93, Jan. 2000
	James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland
	Stefan Edelkamp , Alberto Lluch Lafuente , Stefan Leue, Directed explicit model checking with HSF-SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.57-79, May 2001, Toronto, Ontario, Canada
	Steve Easterbrook , Marsha Chechik, A framework for multi-valued reasoning over inconsistent viewpoints, Proceedings of the 23rd International Conference on Software Engineering, p.411-420, May 12-19, 2001, Toronto, Ontario, Canada
	Emmanuel Letier , Axel van Lamsweerde, Deriving operational software specifications from system goals, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
	Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
	Dimitra Giannakopoulou , Jeff Magee , Jeff Kramer, Checking progress with action priority: is it fair?, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.511-527, Nov. 1999
	Gleb Naumovich , Lori A. Clarke, Classifying properties: an alternative to the safety-liveness classification, ACM SIGSOFT Software Engineering Notes, v.25 n.6, p.159-168, Nov. 2000
	Axel van Lamsweerde, Requirements engineering in the year 00: a research perspective, Proceedings of the 22nd international conference on Software engineering, p.5-19, June 04-11, 2000, Limerick, Ireland
	Tim Menzies , John Powell , Michael E. Houle, Fast formal analysis of requirements via “Topoi Diagrams”, Proceedings of the 23rd International Conference on Software Engineering, p.391-400, May 12-19, 2001, Toronto, Ontario, Canada
	Gerard J. Holzmann, The logic of bugs, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
	Emmanuel Letier , Axel van Lamsweerde, Deriving operational software specifications from system goals, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
	John Hatcliff , Matthew B. Dwyer , Corina S. Păsăreanu , Robby, Foundations of the Bandera abstraction tools, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	John Hatcliff , Xinghua Deng , Matthew B. Dwyer , Georg Jung , Venkatesh Prasad Ranganath, Cadena: an integrated development, analysis, and verification environment for component-based systems, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Dimitra Giannakopoulou , Jeff Magee, Fluent model checking for event-based systems, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
	Radu Iosif , Riccardo Sisto, Temporal logic properties of Java objects, Journal of Systems and Software, v.68 n.3, p.243-251, 15 December 2003
	Shin Nakajima , Tetsuo Tamai, Behavioural analysis of the enterprise JavaBeans component architecture, Proceedings of the 8th international SPIN workshop on Model checking of software, p.163-182, May 2001, Toronto, Ontario, Canada
	Jinlin Yang , David Evans, Dynamically inferring temporal properties, Proceedings of the ACM-SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, June 07-08, 2004, Washington DC, USA
	John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000
	Emmanuel Letier , Axel van Lamsweerde, Reasoning about partial goal satisfaction for requirements and design engineering, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004
	Sascha Konrad , Betty H. C. Cheng , Laura A. Campbell, Object Analysis Patterns for Embedded Systems, IEEE Transactions on Software Engineering, v.30 n.12, p.970-992, December 2004
	Axel van Lamsweerde , Emmanuel Letier, Handling Obstacles in Goal-Oriented Requirements Engineering, IEEE Transactions on Software Engineering, v.26 n.10, p.978-1005, October 2000
	Yu-Tong He , Ryszard Janicki, Verifying protocols by model checking: a case study of the wireless application protocol and the model checker SPIN, Proceedings of the 2004 conference of the Centre for Advanced Studies on Collaborative research, p.174-188, October 04-07, 2004, Markham, Ontario, Canada
	Stephen F. Seigel , George S. Avrunin, Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles, IEEE Transactions on Software Engineering, v.28 n.2, p.115-128, February 2002
	Gaoyan Xie , Cheng Li , Zhe Dang, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Theoretical Computer Science, v.328 n.1-2, p.203-219, 29 November 2004
	Renaud De Landtsheer , Axel van Lamsweerde, Reasoning about confidentiality at requirements engineering time, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
	Wei-Tek Tsai , Lian Yu , Feng Zhu , Ray Paul, Rapid Embedded System Testing Using Verification Patterns, IEEE Software, v.22 n.4, p.68-75, July 2005
	Steven P. Reiss, Specifying and checking component usage, Proceedings of the sixth international symposium on Automated analysis-driven debugging, p.13-22, September 19-21, 2005, Monterey, California, USA
	Sascha Konrad , Betty H. C. Cheng, Real-time specification patterns, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
	Emmanuel Letier , Jeff Kramer , Jeff Magee , Sebastian Uchitel, Fluent temporal logic for discrete-time event-based models, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
	Jeremy S. Bradbury , James R. Cordy , Juergen Dingel, An empirical framework for comparing effectiveness of testing and property-based formal analysis, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
	May Haydar , Sergiy Boroday , Alexandre Petrenko , Houari Sahraoui, Properties and scopes in web model checking, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	Margaret Burnett , Curtis Cook , Omkar Pendse , Gregg Rothermel , Jay Summet , Chris Wallace, End-user software engineering with assertions in the spreadsheet paradigm, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Martin Deubler , Johannes Grünbauer , Jan Jürjens , Guido Wimmel, Sound development of secure service-based systems, Proceedings of the 2nd international conference on Service oriented computing, November 15-19, 2004, New York, NY, USA
	Radu Iosif , Matthew B. Dwyer , John Hatcliff, Translating Java for Multiple Model Checkers: The Bandera Back-End, Formal Methods in System Design, v.26 n.2, p.137-180, March 2005
	Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	M. Autili , P. Inverardi , P. Pelliccione, Graphical scenarios for specifying temporal properties: an automated approach, Automated Software Engineering, v.14 n.3, p.293-340, September 2007
	Borislava I. Simidchieva , Matthew S. Marzilli , Lori A. Clarke , Leon J. Osterweil, Specifying and verifying requirements for election processes, Proceedings of the 2008 international conference on Digital government research, May 18-21, 2008, Montreal, Canada
	Lars Grunske, Specification patterns for probabilistic quality properties, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	M. Autili , P. Inverardi , P. Pelliccione, A scenario based notation for specifying temporal properties, Proceedings of the 2006 international workshop on Scenarios and state machines: models, algorithms, and tools, May 27-27, 2006, Shanghai, China
	Paul Z. Kolano , Richard A. Demmerer, Classification schemes to aid in the analysis of real-time systems, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.86-95, Sept. 2000
	Rachel L. Cobleigh , George S. Avrunin , Lori A. Clarke, User guidance for creating precise and accessible property specifications, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
	Joachim Klein , Christel Baier, Experiments with deterministic ω-automata for formulas of linear temporal logic, Theoretical Computer Science, v.363 n.2, p.182-195, 28 October 2006
	Byron Cook , Alexey Gotsman , Andreas Podelski , Andrey Rybalchenko , Moshe Y. Vardi, Proving that programs eventually do something good, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Hong Liu , David P. Gluch, Templates and automation for temporal query generation, Proceedings of the 44th annual southeast regional conference, March 10-12, 2006, Melbourne, Florida
	Sven Jörges , Tiziana Margaria , Bernhard Steffen, FormulaBuilder: a tool for graph-based modelling and generation of formulae, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Minmin Han , Christine Hofmeister, Modeling and verification of adaptive navigation in web applications, Proceedings of the 6th international conference on Web engineering, July 11-14, 2006, Palo Alto, California, USA
	David Lo , Siau-Cheng Khoo, SMArTIC: towards building an accurate, robust and scalable specification miner, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
	AnnMarie Ericsson , Paul Pettersson , Mikael Berndtsson , Marco Seiriö, Seamless formal verification of complex event processing applications, Proceedings of the 2007 inaugural international conference on Distributed event-based systems, June 20-22, 2007, Toronto, Ontario, Canada
	Kees van Hee , Olivia Oanea , Alexander Serebrenik , Natalia Sidorova , Marc Voorhoeve, LogLogics: A logic for history-dependent business processes, Science of Computer Programming, v.65 n.1, p.30-40, March, 2007
	Massimo Tivoli , Paola Inverardi, Failure-free coordinators synthesis for component-based architectures, Science of Computer Programming, v.71 n.3, p.181-212, May, 2008
	Tomás Barros , Antonio Cansado , Eric Madelaine , Marcela Rivera, Model-checking Distributed Components: The Vercors Platform, Electronic Notes in Theoretical Computer Science (ENTCS), 182, p.3-16, June, 2007
	Matthew B. Dwyer , Alex Kinneer , Sebastian Elbaum, Adaptive Online Program Analysis, Proceedings of the 29th International Conference on Software Engineering, p.220-229, May 20-26, 2007
	Betty H. C. Cheng , Joanne M. Atlee, Research Directions in Requirements Engineering, 2007 Future of Software Engineering, p.285-303, May 23-25, 2007
	Matthew B. Dwyer , Rahul Purandare, Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Zebin Chen , Stephen Fickas, Do No Harm: Model Checking eHome Applications, Proceedings of the 1st International Workshop on Software Engineering for Pervasive Computing Applications, Systems, and Environments, p.8, May 20-26, 2007
	Laura K. Dillon, Automated support for testing and debugging of real-time programs using oracles, ACM SIGSOFT Software Engineering Notes, v.25 n.1, p.45-46, Jan 2000
	Matthew B. Dwyer , John Hatcliff, Adapting programming languages technologies for finite-state verification, ACM SIGSOFT Software Engineering Notes, v.25 n.1, p.46-49, Jan 2000
	Axel van Lamsweerde, Elaborating Security Requirements by Construction of Intentional Anti-Models, Proceedings of the 26th International Conference on Software Engineering, p.148-157, May 23-28, 2004
	A. Alfonso , V. Braberman , N. Kicillof , A. Olivero, Visual Timed Event Scenarios, Proceedings of the 26th International Conference on Software Engineering, p.168-177, May 23-28, 2004
	Yves Bontemps , Pierre-Yves Schobbens , Christof Löding, Synthesis of Open Reactive Systems from Scenario-Based Specifications, Fundamenta Informaticae, v.62 n.2, p.139-169, April 2004
	Marco Autili , Patrizio Pelliccione, Towards a Graphical Tool for Refining User to System Requirements, Electronic Notes in Theoretical Computer Science (ENTCS), 211, p.147-157, April, 2008
	Anne Remke , Boudewijn R. Haverkort , Lucia Cloth, CSL model checking algorithms for QBDs, Theoretical Computer Science, v.382 n.1, p.24-41, August, 2007
	Lori A. Clarke , George A. Avrunin , Leon J. Osterweil, Using software engineering technology to improve the quality of medical processes, Companion of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Yuan Gan , Marsha Chechik , Shiva Nejati , Jon Bennett , Bill O'Farrell , Julie Waterhouse, Runtime monitoring of web service conversations, Proceedings of the 2007 conference of the center for advanced studies on Collaborative research, October 22-25, 2007, Richmond Hill, Ontario, Canada
	Ke Xu , Ying Liu , Cheng Wu, BPSL Modeler -- Visual Notation Language for Intuitive Business Property Reasoning, Electronic Notes in Theoretical Computer Science (ENTCS), 211, p.211-220, April, 2008
	Ayman Mahfouz , Leonor Barroca , Robin Laney , Bashar Nuseibeh, Patterns for service-oriented information exchange requirements, Proceedings of the 2006 conference on Pattern languages of programs, October 21-23, 2006, Portland, Oregon
	Pablo Moreno-Ger , Rubén Fuentes-Fernández , José-Luis Sierra-Rodríguez , Baltasar Fernández-Manjón, Original papers: Model-checking for adventure videogames, Information and Software Technology, v.51 n.3, p.564-580, March, 2009
	David Lo , Siau-Cheng Khoo , Chao Liu, Mining past-time temporal rules from execution traces, Proceedings of the 2008 international workshop on dynamic analysis: held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2008), July 21-21, 2008, Seattle, Washington
	Robert Colvin , Lars Grunske , Kirsten Winter, Timed Behavior Trees for Failure Mode and Effects Analysis of time-critical systems, Journal of Systems and Software, v.81 n.12, p.2163-2182, December, 2008
	José C. Campos , Michael D. Harrison, Interaction engineering using the IVY tool, Proceedings of the 1st ACM SIGCHI symposium on Engineering interactive computing systems, July 15-17, 2009, Pittsburgh, PA, USA
	Peter Y. H. Wong , Jeremy Gibbons, A Relative Timed Semantics for BPMN, Electronic Notes in Theoretical Computer Science (ENTCS), v.229 n.2, p.59-75, July, 2009
	P. Bellini , P. Nesi , D. Rogai, Expressing and organizing real-time specification patterns via temporal logics, Journal of Systems and Software, v.82 n.2, p.183-196, February, 2009
	Kees van Hee , Alexander Serebrenik , Natalia Sidorova, Token History Petri Nets, Fundamenta Informaticae, v.85 n.1-4, p.219-234, September 2008
	Franz Weitl , Mirjana Jakšić , Burkhard Freitag, Towards the automated verification of semi-structured documents, Data & Knowledge Engineering, v.68 n.3, p.292-317, March, 2009
	Tomas Matousek , Pavel Jezek, DeSpec: Modeling the Windows Driver Environment11This work was partially supported by the Czech Academy of Sciences project 1ET400300504 and the Grant Agency of the Czech Republic project GD201/05/H014., Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.7, p.55-69, April, 2009
	David Lo , Siau-Cheng Khoo , Chao Liu, Mining temporal rules for software maintenance, Journal of Software Maintenance and Evolution: Research and Practice, v.20 n.4, p.227-247, July 2008
	Jian Yu , Yan-Bo Han , Jun Han , Yan Jin , Paolo Falcarin , Maurizio Morisio, Synthesizing service composition models on the basis of temporal business rules, Journal of Computer Science and Technology, v.23 n.6, p.885-894, November 2008
	Pedro T. Monteiro , Delphine Ropers , Radu Mateescu , Ana T. Freitas , Hidde de Jong, Temporal Logic Patterns for Querying Qualitative Models of Genetic Regulatory Networks, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.229-233, June 27, 2008
	Tao Huang , Guo-Quan Wu , Jun Wei, Runtime monitoring composite web services through stateful aspect extension, Journal of Computer Science and Technology, v.24 n.2, p.294-308, March 2009
	Yasuyuki Tahara , Nobukazu Yoshioka , Kenji Taguchi , Toshiaki Aoki , Shinichi Honiden, Evolution of a course on model checking for practical applications, ACM SIGCSE Bulletin, v.41 n.2, June 2009
	Victor Braberman , Nicolas Kicillof , Alfredo Olivero, A Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties, IEEE Transactions on Software Engineering, v.31 n.12, p.1028-1041, December 2005