Modeling and Specification of Real-Time Interfaces with UTP
详细信息    查看全文
  • 作者:Hung Dang Van (19)
    Hoang Truong (19)
  • 刊名:Lecture Notes in Computer Science
  • 出版年:2013
  • 出版时间:2013
  • 年:2013
  • 卷:8051
  • 期:1
  • 页码:151-165
  • 全文大小:302KB
  • 参考文献:1. de Alfaro, L., Henzinger, T.A.: Interface Automata. In: ACM Symposium on Foundation of Software Engineering, FSE (2001)
    2. Doyen, L., Henzinger, T.A., Jobstmann, B., Petrov, T.: Interface theories with component reuse. In: EMSOFT, pp. 79鈥?8 (2008)
    3. Van Hung, D.: Toward a formal model for component interfaces for real-time systems. In: Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2005, pp. 106鈥?14. ACM, New York (2005) CrossRef
    4. He, J., Liu, Z., Li, X.: rCOS: A refinement calculus of object systems. Theor. Comput. Sci., 365(1-2), 109鈥?42 (2006), UNU-IIST TR 322
    5. Ledang, H., Van Hung, D.: Timing and concurrency specification in component-based real-time embedded systems development. In: TASE, pp. 293鈥?04. IEEE Computer Society (2007)
    6. Chen, X., He, J., Liu, Z., Zhan, N.: A model of component-based programming. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol.聽4767, pp. 191鈥?06. Springer, Heidelberg (2007) CrossRef
    7. Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. ACM Transactions on Programming Languages and Systems聽33(4) (2011)
    8. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Series in Computer Science, Prentice Hall (1998)
    9. Wang, S., Rho, S., Mai, Z., Bettati, R., Zhao, W.: Real-time component-based systems. In: Proceedings of the 11th IEEE Real Time and Embedded Technology and Applications Symposium, RTAS 2005, pp. 1080鈥?812. IEEE Computer Society (2005)
    10. Henzinger, T.A., Matic, S.: An interface algebra for real-time components. In: IEEE Real Time Technology and Applications Symposium, pp. 253鈥?66 (2006)
    11. Delahaye, B., Fahrenberg, U., Henzinger, T.A., Legay, A., Ni膷kovi膰, D.: Synchronous interface theories and time triggered scheduling. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE 2012. LNCS, vol.聽7273, pp. 203鈥?18. Springer, Heidelberg (2012) CrossRef
    12. Wiklander, J., Eliasson, J., Kruglyak, A., Lindgren, P., Nordlander, J.: Enabling component-based design for embedded real-time software. Journal of Computers聽4(12), 1039鈥?321 (2009) CrossRef
    13. Van Hung, D., Vu Anh, B.: Model checking real-time component based systems with blackbox testing. In: RTCSA, pp. 76鈥?9 (2005)
    14. Truong, A.-H., Trinh, T.-B., Van Hung, D., Nguyen, V.-H., Trang, N.T.T., Hung, P.D.: Checking interface interaction protocols using aspect-oriented programming. In: Software Engineering and Formal Methods (SEFM 2008), pp. 382鈥?86 (2008)
  • 作者单位:Hung Dang Van (19)
    Hoang Truong (19)

    19. University of Engineering and Technology, Vietnam National University, Hanoi, Vietnam
文摘
Interface modeling and specification are central issues of component-based software engineering. How a component will be used is specified in its interface. Real-time interfaces are interfaces with timing constraints relating the time of outputs with the time of inputs. The timing constraint of an interface may depend on the resource availability for the component. In this paper, we propose a general model for real-time interfaces. At a time during execution, an interface behaves according to a contract made with environment about its functionality as well as execution time to fulfill the contract. This contract is specified as a timed design using the UTP notations, and depends on the computation histories of the interface. We model this dependence as a partial function from computation histories of the interface to real-time contracts. How interfaces are composed to form new interfaces, how interfaces are refined, and how to represent interfaces finitely are also considered in this paper. We show that checking the consistency between an environment and an interface and checking the refinement between two interfaces when they are represented by an automaton can be done effectively.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700