Templates and automation for temporal query generation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Templates and automation for temporal query generation

Full text

Pdf (126 KB)

Source

ACM Southeast Regional Conference archive
Proceedings of the 44th annual Southeast regional conference table of contents

Melbourne, Florida

SESSION: Software engineering I table of contents

Pages: 80 - 84

Year of Publication: 2006

ISBN:1-59593-315-8

Authors

Hong Liu	Embry-Riddle Aeronautical University, Daytona Beach, FI
David P. Gluch	Embry-Riddle Aeronautical University, Daytona Beach, FI

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 27, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/1185448.1185467 What is a DOI?

ABSTRACT

This paper presents preliminary results in defining templates and a framework for an automation tool for generating temporal logic queries from the expected properties of requirements documents specified in natural Language. Specifically, we first extend the theoretic results published in [16]from Linear Temporal Logic (LTL) to Computation Tree Logic (CTL). Then we present a template to elicit informal queries in a form that can be automatically mapped to either LTL or CTL queries. These efforts are the foundation for the development of a Java-based formal query generation tool that will facilitate the generation of formal queries from informal specifications. The tool will be integrated into the OSATE Eclipse-based analysis and design environment for the Society of Automotive Engineers (SAE) standard---the Architecture Analysis & Design Language (AADL) [1].

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	The SAE Architecture Analysis & Design Language (AADL) www.aadl.info.
	2	J. Callahan, F. Schneider, and S. Easterbrook, Specification-based using model checking: In Proc. SPIN Workshop, Utger University, August 1996, Tech. Report, NASA-IVV-96-022.
	3	Edmund M. Clarke and Jeannette, M. Wing, Formal Methods: State pf the Art and Future Directions, Publication Depts. ACM, Inc., 1515 Broadway, New York, NY 10036.
	4	Comella-Dorda, S., David P. Gluch, et al., Model-Based Verification: Claim Creation Guidelines, (CMU/SEI-2001-TN-018). Pittsburgh, Pa.: Software Engineering Institute, Carnegie Mellon University, October 2001.
	5	Dov Dori, Object-Process Methodology, Springer, 2002. www.ObjectProcess.org.
	6	Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
	7	Feiler, P. H.; Gluch, D. P.; Hudak, J. J.; Lewis, B. A. "Pattern-Based Analysis of an Embedded Real-time System Architecture," Proceedings of the Workshop on Architecture Description Languages (WADL04) at the IFIP World Computer Congress August, 27 2004.
	8	Feiler, P.; Gluch, D.; Hudak, J.; Lewis, B. Embedded Systems Architecture Analysis Using SAE AADL, Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, Technical Note: CMU/SEI-2004-TN-005, June, 2004.
	9	Gluch, D. P., Comella-Dorda, S., Hudak, J.; Lewis, G.; & Weinstock, C., Model-Based Verification: Guidelines for Generating Expected Properties, (CMU/SEI-2002-TN-003), Pittsburgh, Pa. Software Engineering Institute, Carnegie Mellon University, 2002.
	10	Hai Huang , Wei-Tek Tsai , Raymond Paul , Yinong Chen, Automated Model Checking and Testing for Composite Web Services, Proceedings of the Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05), p.300-307, May 18-20, 2005 [doi>10.1109/ISORC.2005.16]
	11	I-Logic, Pattern Library of Model Certifier, white paper published on {www.i-Logic.com}.
	12	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	13	Lewis, G.; Comella-Dorda, S; Gluch, D. P.; Hudak, J.; & Weinstock, C., Model-Based Verification: Analysis Guidelines, (CMU/SEI-2001-TN-028). Pittsburgh, Pa.: Software Engineering Institute, Carnegie Mellon University, December 2001.
	14	Hong Liu , David P. Gluch, A proposal for introducing model checking into an undergraduate software engineering curriculum, Journal of Computing Sciences in Colleges, v.18 n.2, p.259-270, December 2002
	15	Hong Liu , David P. Gluch, Conceptual modeling with the object-process methodology in software architecture, Journal of Computing Sciences in Colleges, v.19 n.3, p.10-21, January 2004
	16	H. Liu, D. P. Gluch, Query Generation Guidelines and Consideration to Statecharts of Object-Oriented Designs, Proceeding of the Conference of Advances in Computer Sciences and Technology sponsored by IASTED (International Association of Science and Technology For Development). 11, 2004, Page 209--214.
	17	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	18	K. Myers, K. Dionne, V. Vijay, S. Dunlap, D. P. Gluch., "The Practical Use of Model Checking in Software Development", Proceedings IEEE Southeast Conference, 2002, 0-7803-7252-2/02, P. 21--27.
	19	Property Specification Language Reference Manual, Accellera, Version 1.1, 2004.
	20	W. T. Tsai, R. Paul, B. Xiao, Z. Cao, Y. Chen, "PSML-S: A Process Specification and Modeling Language for Service Oriented Computing", The 9th IASTED International Conference on Software Engineering and Application (SEA), Phoenix, November 2005.