Design and specification of embedded systems in Java using successive, formal refinement

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Design and specification of embedded systems in Java using successive, formal refinement

Full text

Pdf (257 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 35th annual Design Automation Conference table of contents

San Francisco, California, United States

Pages: 70 - 75

Year of Publication: 1998

ISBN:0-89791-964-5

Authors

James Shin Young	Department of Electrical Engineering and Computer Sciences, University of California, Berkeley
Josh MacDonald	Department of Electrical Engineering and Computer Sciences, University of California, Berkeley
Michael Shilman	Department of Electrical Engineering and Computer Sciences, University of California, Berkeley
Abdallah Tabbara	Department of Electrical Engineering and Computer Sciences, University of California, Berkeley
Paul Hilfinger	Department of Electrical Engineering and Computer Sciences, University of California, Berkeley
A. Richard Newton	Department of Electrical Engineering and Computer Sciences, University of California, Berkeley

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
EDAC : Electronic Design Automation Consortium
IEEE-CS : Computer Society

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 16, Citation Count: 18

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/277044.277058 What is a DOI?

ABSTRACT

Successive, formal refinement is a new approach for specificationof embedded systems using a general-purpose programming language.Systems are formally modeled as Abstractable SynchronousReactive systems, and Java is used as the design inputlanguage. A policy of use is applied to Java, in the form of languageusage restrictions and class-library extensions, to ensureconsistency with the formal model. A process of incremental,user-guided program transformation is used to refine a Java programuntil it is consistent with the policy of use. The final productis a system specification possessing the properties of the formalmodel, including deterministic behavior, bounded memory usage,and bounded execution time. This approach allows systems designto begin with the flexibility of a general-purpose language, followedby gradual refinement into a more restricted form necessaryfor specification.

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	Friedrich Ludwig Bauer , Bernhard Möller , Helmut Partsch , Peter Pepper, Formal Program Construction by Transformations-Computer-Aided, Intuition-Guided Programming, IEEE Transactions on Software Engineering, v.15 n.2, p.165-180, February 1989 [doi>10.1109/32.21743]
	2	A. Benveniste and G. Berry, "The Synchronous Approach to Reactive and Real-Time Systems,"Proc. IEEE, 79(9):1270- !282, September 1991.
	3	Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
	4	Stephen Anthony Edwards, The specification and execution of heterogeneous synchronous reactive systems, University of California at Berkeley, Berkeley, CA, 1998
	5	Daniel D. Gajski , Frank Vahid , Sanjiv Narayan , Jie Gong, Specification and design of embedded systems, Prentice-Hall, Inc., Upper Saddle River, NJ, 1994
	6	James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
	7	CN. Halbwachs, et. al. The synchronous data flow programming language LUSTRE. Prec. of the IEEE, 79(9):1305- 1320, 1991.
	8	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	9	D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
	10	Rachid Helaihel , Kunle Olukotun, Java as a specification language for hardware-software systems, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.690-697, November 09-13, 1997, San Jose, California, United States
	11	Stan Liao , Steve Tjiang , Rajesh Gupta, An efficient implementation of reactivity for modeling hardware in the scenic design environment, Proceedings of the 34th annual conference on Design automation, p.70-75, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266037]
	12	James A. Rowson , Alberto Sangiovanni-Vincentelli, Interface-based design, Proceedings of the 34th annual conference on Design automation, p.178-183, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266060]
	13	D. R. Smith, KIDS: A Semiautomatic Program Development System, IEEE Transactions on Software Engineering, v.16 n.9, p.1024-1043, September 1990 [doi>10.1109/32.58788]

CITED BY 18

	Diederik Verkest , Joachim Kunkel , Frank Schirrmeister, System level design using C++, Proceedings of the conference on Design, automation and test in Europe, p.74-83, March 27-30, 2000, Paris, France
	T. Kuhn , T. Oppold , M. Winterholer , W. Rosenstiel , Marc Edwards , Yaron Kashai, A framework for object oriented hardware specification, verification, and synthesis, Proceedings of the 38th conference on Design automation, p.413-418, June 2001, Las Vegas, Nevada, United States
	Tommy Kuhn , Wolfgang Rosenstiel, Java based object oriented hardware specification and synthesis, Proceedings of the 2000 conference on Asia South Pacific design automation, p.579-582, January 2000, Yokohama, Japan
	David F. Bacon, Kava: a Java dialect with a uniform object model for lightweight classes, Proceedings of the 2001 joint ACM-ISCOPE conference on Java Grande, p.68-77, June 2001, Palo Alto, California, United States
	Axel Jantsch , Per Bjuréus, Composite signal flow: a computational model combining events, sampled streams, and vectors, Proceedings of the conference on Design, automation and test in Europe, p.154-160, March 27-30, 2000, Paris, France
	P. Coste , F. Hessel , Ph. Le Marrec , Z. Sugar , M. Romdhani , R. Suescun , N. Zergainoh , A. A. Jarraya, Multilanguage design of heterogeneous systems, Proceedings of the seventh international workshop on Hardware/software codesign, p.54-58, March 1999, Rome, Italy
	T. Kuhn , T. Oppold , C. Schulz-Key , M. Winterholer , W. Rosenstiel , M. Edwards , Y. Kashai, Object oriented hardware synthesis and verification, Proceedings of the 14th international symposium on Systems synthesis, September 30-October 03, 2001, Montréal, P.Q., Canada
	Cindy Eisner , Irit Shitsevalov , Russ Hoover , Wayne Nation , Kyle Nelson , Ken Valk, A methodology for formal design of hardware control with application to cache coherence protocols, Proceedings of the 37th conference on Design automation, p.724-729, June 05-09, 2000, Los Angeles, California, United States
	Sérgio Akira Ito , Luigi Carro , Ricardo Pezzuol Jacobi, System design based on single language and single-chip Java ASIP microcontroller, Proceedings of the conference on Design, automation and test in Europe, p.703-709, March 27-30, 2000, Paris, France
	Josef Fleischmann , Klaus Buchenrieder , Rainer Kress, Java driven codesign and prototyping of networked embedded systems, Proceedings of the 36th ACM/IEEE conference on Design automation, p.794-797, June 21-25, 1999, New Orleans, Louisiana, United States
	Marcello Dalpasso , Alessandro Bogliolo , Luca Benini, Virtual simulation of distributed IP-based designs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.50-55, June 21-25, 1999, New Orleans, Louisiana, United States
	Annette Bunker , Ganesh Gopalakrishnan , Sally A. Mckee, Formal hardware specification languages for protocol compliance verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.9 n.1, p.1-32, January 2004
	Tony Givargis , Frank Vahid , Jörg Henkel, A hybrid approach for core-based system-level power modeling, Proceedings of the 2000 conference on Asia South Pacific design automation, p.141-146, January 2000, Yokohama, Japan
	Tommy Kuhn , Wolfgang Rosenstiel , Udo Kebschull, Description and simulation of hardware/software systems with Java, Proceedings of the 36th ACM/IEEE conference on Design automation, p.790-793, June 21-25, 1999, New Orleans, Louisiana, United States
	C. Schulz-Key , M. Winterholer , T. Schweizer , T. Kuhn , W. Rosenstiel, Object-oriented modeling and synthesis of SystemC specifications, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.238-243, January 27-30, 2004, Yokohama, Japan
	Sérgio Akira Ito , Luigi Carro , Ricardo Pezzuol Jacobi, Making Java Work for Microcontroller Applications, IEEE Design & Test, v.18 n.5, p.100-110, September 2001
	Jianwen Zhu , Daniel D. Gajski, OpenJ: an extensible system level design language, Proceedings of the conference on Design, automation and test in Europe, p.99-es, January 1999, Munich, Germany
	Marcello Dalpasso , Alessandro Bogliolo , Luca Benini, Specification and validation of disstributed IP-based designs with JavaCAD, Proceedings of the conference on Design, automation and test in Europe, p.132-es, January 1999, Munich, Germany