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

被引：0
|
作者：
Young, JS [1 ]
MacDonald, J [1 ]
Shilman, M [1 ]
Tabbara, A [1 ]
Hilfinger, P [1 ]
Newton, AR [1 ]
机构：
[1] Univ Calif Berkeley, Dept Elect Engn & Comp Sci, Berkeley, CA 94720 USA
来源：
1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS | 1998年
关键词：
D O I：
暂无
中图分类号：
T [工业技术];
学科分类号：
08 ;
摘要：
Successive, formal refinement is a new approach for specification of embedded systems using a general-purpose programming language. Systems are formally modeled as Abstractable Synchronous Reactive systems, and Java is used as the design input language. A policy of use is applied to Java, in the form of language usage restrictions and class-library extensions, to ensure consistency with the formal model. A process of incremental, user-guided program transformation is used to refine a Java program until it is consistent with the policy of use. The final product is a system specification possessing the properties of the formal model, including deterministic behavior, bounded memory usage and bounded execution time. This approach allows systems design to begin with the flexibility of a general-purpose language, followed by gradual refinement into a more restricted form necessary for specification.
引用
收藏
页码：70 / 75
页数：6
相关论文
共 50 条
  • [1] Java']Java in embedded-systems design
    Varhol, P
    [J]. COMPUTER DESIGN, 1997, 36 (03): : 63 - +
  • [2] A formal specification of Java']Java™ class leading
    Qian, ZY
    Goldberg, A
    Coglio, A
    [J]. ACM SIGPLAN NOTICES, 2000, 35 (10) : 325 - 336
  • [3] Formal specification and verification of Java']Java refactorings
    Garrido, Alejandra
    Meseguer, Jose
    [J]. SIXTH IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2006, : 165 - +
  • [4] A formal specification in JML of Java']Java security package
    Agarwal, Poonam
    Rubio-Medrano, Carlos E.
    Cheon, Yoonsik
    Teller, Patricia. J.
    [J]. ADVANCES AND INNOVATIONS IN SYSTEMS, COMPUTING SCIENCES AND SOFTWARE ENGINEERING, 2007, : 363 - 368
  • [5] Java']Java for embedded systems
    Mulchandani, D
    [J]. IEEE INTERNET COMPUTING, 1998, 2 (03) : 30 - 39
  • [6] Formal specification of Java']JavaSpaces™ architecture using μCRL
    van de Pol, J
    Espada, MV
    [J]. COORDINATION MODELS AND LANGUAGES, PROCEEDINGS, 2002, 2315 : 274 - 290
  • [7] Discovering anomalies in access modifiers in Java']Java with a formal specification
    Yang, W
    [J]. JOOP-JOURNAL OF OBJECT-ORIENTED PROGRAMMING, 2001, 13 (10): : 12 - 18
  • [8] Certifying native Java']Java Card API by formal refinement
    Nguyen, QH
    Chetali, B
    [J]. SMART CARD RESEARCH AND ADVANCED APPLICATIONS, PROCEEDINGS, 2006, 3928 : 313 - 328
  • [9] A formal specification of Java™ class loading
    Qian, Z.
    Goldberg, A.
    Coglio, A.
    [J]. Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA, 2000, 35 (10): : 325 - 336
  • [10] Adapting Java']Java for embedded systems
    Varhol, P
    [J]. COMPUTER DESIGN, 1997, 36 (10): : 75 - +
12345