Verification and semantic parallelization of goal-driven autonomous software

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verification and semantic parallelization of goal-driven autonomous software

Full text

Pdf (275 KB)

Source

International Conference on Autonomic Computing and Communication Systems archive
Proceedings of the 2nd International Conference on Autonomic Computing and Communication Systems table of contents

Turin, Italy

Article No. 33

Year of Publication: 2008

ISBN:978-963-9799-34-9

Authors

Damian Dechev	Texas A&M University, College Station, TX
Nicolas Rouquette	California Institute of Technology, Pasadena, CA
Peter Pirkelbauer	Texas A&M University, College Station, TX
Bjarne Stroustrup	Texas A&M University, College Station, TX

Sponsors

: ICST
ACM: Association for Computing Machinery
: Create-Net

Publisher

ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering) ICST, Brussels, Belgium, Belgium

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 32, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

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

ABSTRACT

Future space missions such as the Mars Science Laboratory demand the engineering of some of the most complex man-rated autonomous software systems. According to some recent estimates, the certification cost for mission-critical software exceeds its development cost. The current process-oriented methodologies do not reach the level of detail of providing guidelines for the development and validation of concurrent software. Time and concurrency are the most critical notions in an autonomous space system. In this work we present the design and implementation of a first concurrency and time centered framework for verification and semantic parallelization of real-time C++ within the JPL Mission Data System Framework (MDS). The end goal of the industrial project that motivated our work is to provide certification artifacts and accelerated testing of the complex software interactions in autonomous flight systems. As a case study we demonstrate the verification and semantic parallelization of the MDS Goal Networks.

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	Barry Boehm , Jesal Bhuta , David Garlan , Eric Gradman , LiGuo Huang , Alexander Lam , Ray Madachy , Nenad Medvidovic , Kenneth Meyer , Steven Meyers , Gustavo Perez , Kirk Reinholtz , Roshanak Roshandel , Nicolas Rouquette, Using Empirical Testbeds to Accelerate Technology Maturity and Transition: The SCRover Experience, Proceedings of the 2004 International Symposium on Empirical Software Engineering, p.117-126, August 19-20, 2004 [doi>10.1109/ISESE.2004.33]
	2	Guillaume Brat , Doron Drusinsky , Dimitra Giannakopoulou , Allen Goldberg , Klaus Havelund , Mike Lowry , Corina Pasareanu , Arnaud Venet , Willem Visser , Rich Washington, Experimental Evaluation of Verification and Validation Tools on Martian Rover Software, Formal Methods in System Design, v.25 n.2-3, p.167-198, September-November 2004 [doi>10.1023/B:FORM.0000040027.28662.a4]
	3	Columbia Accident Investigation Board. Columbia Accident Investigation Board Report Volume 1.
	4	Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
	5	D. Dechev, P. Pirkelbauer, and B. Stroustrup. Lock-Free Dynamically Resizable Arrays. In A. A. Shvartsman, editor, OPODIS, volume 4305 of Lecture Notes in Computer Science, pages 142--156. Springer, 2006.
	6	Ewen Denney , Bernd Fischer , Dieter Hutter , Mark Jones, Software certificate management (SoftCeMent'05), Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1102003]
	7	Robert P. Dick , David L. Rhodes , Wayne Wolf, TGFF: task graphs for free, Proceedings of the 6th international workshop on Hardware/software codesign, p.97-101, March 15-18, 1998, Seattle, Washington, United States
	8	D. Dvorak. Challenging encapsulation in the design of high-risk control systems. In Proceedings of the 17th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'02), 2002.
	9	D. Dvorak, G. Bollella, T. Canham, V. Carson, V. Champlin, B. Giovannoni, M. Indictor, K. Meyer, A. Murray, and K. Reiinholtz. Project Golden Gate: Towards Real-Time Java in Space Missions. In In the Proceedings of the 7th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'04), 2004.
	10	R. Gluck and G. Holzmann. Using the spin model checker for flight software verification. In Proceedings of the 2002 IEEE Aerospace Conference, 2002.
	11	M. Herlihy, A methodology for implementing highly concurrent data structures, Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming, p.197-206, March 14-16, 1990, Seattle, Washington, United States
	12	Intel. Reference for Intel Threading Building Blocks, version 1.0, April 2006.
	13	Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
	14	E. Lee and S. Neuendorffer. Concurrent Models of computation for Embedded Software. In IEEE Proceedings on Computers and Digital Techniques, March 2005.
	15	J. Lou. An Efficient Algorithm for Propagation of Temporal Constraint Networks. NASA Tech Brief Vol. 26 No. 4 from JPL New Technology Report NPO-21098, April 2002.
	16	Michael R. Lowry, Software Construction and Analysis Tools for Future Space Missions, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.1-19, April 08-12, 2002
	17	C. Perrow. Normal Accidents. Princeton University Press, September 1999.
	18	R. Rasmussen, M. Ingham, and D. Dvorak. Achieving Control and Interoperability Through Unified Model-Based Engineering and Software Engineering. In AIAA Infotech at Aerospace Conference, 2005.
	19	G. D. Reis and B. Stroustrup. Specifying C++ Concepts, ISO WG21 N1886, 2005.
	20	N. Rouquette. Analyzing and verifying UML models with OCL and Alloy. EclipseCon 2008, 2008.
	21	RTCA. Software Considerations in Airborne Systems and Equipment Certification (DO-178B), 1992.
	22	J. Schumann and W. Visser. Autonomy Software: V&V Challenges and Characteristics. In Proceedings of the 2006 IEEE Aerospace Conference, 2006.
	23	Bjarne Stroustrup, The C++ Programming Language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
	24	B. Stroustrup and G. D. Reis. Supporting SELL for High-Performance Computing. In Proceedings of the International Workshop on Languages and Compilers for Parallel Computing, LCPC 2005, 2005.
	25	R. Volpe, I. Nesnas, T. Estlin, D. Mutz, R. Petras, and H. Das. The CLARAty Architecture for Robotic Autonomy. In IEEE Aerospace Conference, March 2001.