微信服务号

微信订阅号

2025-4-16- 16
Home > Archive>Volume 10, Issue 10, 1999 >1025-1031
PDF HTML XML Export Cite reminder
T3BDD Based Dynamic Model Checking
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [1]
    • |
  • Related
    • | | |
  • Comments
    Abstract:

    Java Beans is a standard for software components. For checking the consistency of the Java Beans semantic constraints with its implementation, a formal Java Beans description language (JBDL) and a dynamic model checking method are proposed in this paper. The authors contribute an efficient symbolic model checking approach using T3BDD. The approach is based on three valued semantics for JBDL formulas and a kind of abstract model which is dynamically established and evolved during Bean’s execution.

    Reference
    1　 Shenker S, Wroclawski J. Network element service specification template. IETF C 2216, September 1997 2　 林闯.ATM网络一种实时传输调度和分组丢失控制的综合方案.计算机学报,1998,21(4):333～340(Lin Chuang. Integration of traffic scheduling and cell loss control in ATM networks. Chinese Journal of Computers, 1998,21(4):333～340) 3　 Reisslein M, Ross K W, Rajagopal S. Guaranteeing statistical QoS to regulated traffic: the single node case. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99). New York: IEEE Computer Society, 1999. 1601～1072 4　 Lin Chuang, Chanson S T. ATM admission models of stochastic high level Petri nets based on hierarchical modeling. In: Proceedings of 1995 International Conference on Network Protocols. Tokyo: IEEE Computer Society, 1995. 144～151 5　 林闯,张元生.基于随机高级Petri网的ATM网络接纳控制过程模型.通信学报,1998,19(12):1～7(Lin Chuang, Zhang Yuan-sheng. Modeling ATM admission control procedures using stochastic high level Petri nets. Journal of China Institute of Communications, 1998,19(12):1～7) 6　 Kurz T, Thiran P, Boudec J L. Regulation of a connection admission control algorithm. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99). New York: IEEE Computer Society, 1999. 1053～1060 7　 Knightly E W. Enforceable quality of service guarantees for bursty traffic streams. In: Proceedings of the 17th Annual Joint Conference of the IEEE 　　Computer and Communications Societies (IEEE INFOCOM’98). San Francisco,CA: IEEE　Computer Society, 1998. 635～642 8　 Shenker S, Partridge C, Guerin R.Specification of guaranteed quality of service.IETF RFC 2212, September 1997 9　 Crawley E, Nair R, Rajagopalan B et al. A framework for QoS-based routing in the　internet. IETF RFC 2386, August 1998 10　 Cidon I, Rom R. Multi-path routing combined with resource reservation. In: Proceedings of the 16th Annual Joint Conference of the IEEE Computer and S922 Communications Societies (IEEE INFOCOM’97). Kobe: IEEE Computer Society, 1997. 92～100 11　 Braden R, Zhang L, Berson S et al. Resource ReSerVation Protocol(RSVP)(Version 1): Function Specification. IETF RFC 2205, September 1997 12　 Rao N S V, Batsell S G. QoS routing via multiple paths using bandwidth reservation. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). San Francisco, CA: IEEE Computer Society, 1998. 11～18 13　 Orda A. Routing with end to end QoS guarantees in broadband networks. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). San Francisco, CA: IEEE Computer Society, 1998. 27～34 14　 Su C F, Veciana G. On statistical multiplexing, traffic mixes, and VP management. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). San Francisco, CA: IEEE Computer Society, 1998. 643～650 15　 Lorenz D H, Orda A. QoS routing in networks with uncertain parameters. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). San Francisco, CA: IEEE Computer Society, 1998. 3～10 16　 Apostolopoulos G, Guerin R, Kamat S. Implementation and performance measurements of QoS routing extensions to OSPF. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99). New York: IEEE Computer Society, 1999. 680～688 17　 Toutain F. Decoupled generalized processor sharing: a fair queuing principle for adaptive multimedia applications. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM'98).San Francisco, CA: IEEE Computer Society, 1998. 291～298 18　 Chiussi F M, Francini A. Implementing fair queuing in ATM switches: the discrete-rate approach. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98).San Francisco,CA: IEEE Computer Society, 1998. 272～281 19　 Golestani S J. A self-clocked fair queuing scheme for broadband applications. In: Proceedings of the 13th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’94). Toronto: IEEE Computer Society, 1994. 636～646 20　 Bennett J C R, Zhang H. WF2Q: worst-case fair weighted fair queuing. In: Proceedings of the 15th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’96). San Francisco, CA: IEEE Computer Society, 1996. 120～128 21　 Andrews M, Zhang L. Minimizing end-to-end delay in high-speed networks with a simple coordinated schedule. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99). New York: IEEE Computer Society, 1999. 380～388 22　 Braden R, Clark D, Shenker S. Integrated services in the internet architecture: an overview. IETF RFC 1633, June 1994 23　 Wroclawski J. Specification of the controlled-load network element service. IETF RFC 2211, September 1997 24　 Nichols K, Jacobson V, Zhang L. A two-bit differentiated services architecture for the internet. IETF Internet Draft ＜ draft-nichols-diff-svc-arch-00.tex＞ , Nov. 1997 25　 Wroclawski J. The use of RSVP with IETF integrated services. IETF RFC 2210, September 1997 26　 Ma Q, Steenkiste P. Supporting dynamic inter-class resource sharing: a multi-class QoS routing algorithm. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99).ew York: IEEE Computer Society, 1999. 649～660 27　 Elwalid A, Mitra D. Design of generalized processor sharing schedulers which statistically multiplex heterogeneous QoS classes. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99). New York: IEEE Computer Society, 1999. 1220～1230 28　 Lin D. Constant-time dynamic ATM bandwidth scheduling for guaranteed and best effort services with overbooking. In: Proceedings of the 16th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’97). 　　Kobe: IEEE Computer Society, 1997. 398～405 29　 Li B, Lin C, Chanson S T. Analysis of a hybrid cutoff priority scheme for ultiple classes of traffic in multimedia wireless networks. ACM Journal of ireless Networks, 1998,4(4):279～290 30　 Cruz R L. SCED+: efficient management of quality of service guarantees. In: Proceedings of the 17th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). San Francisco, CA: IEEE Computer 　　Society, 1998. 625～634　31　 Chang C S, Cruz R L. A time varying filtering theory for constrained traffic regulation and dynamic service guarantees. In: Proceedings of the 18th Annual Joint Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’99). New York: IEEE Computer Society, 1999. 63～70 32　 Mithal S. Bounds on end-to-end performance via greedy, multi-path routing in 　　integrated services networks. In: Proceedings of the 17th Annual Joint 　　Conference of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). 　　San Francisco, CA: IEEE Computer Society, 1998. 19～26 33　 林闯.ATM网络基于队列长度阈值的传输调度.软件学报,1998,9(4):316～320 　　(Lin Chuang. Traffic scheduling based on the queue length threshold in ATM 　　networks. Journal of Software, 1998,9(4):316～320) 34　 Altman E, Orda A, Shimkin N. Bandwidth allocation for guaranteed versus best 　　effort service categories. In: Proceedings of the 17th Annual Joint Conference 　　of the IEEE Computer and Communications Societies (IEEE INFOCOM’98). San 　　Francisco, CA: IEEE Computer Society, 1998. 617～624
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

倪 彬,冯玉琳,黄 涛.基于T3BDD的动态模型检查*.软件学报,1999,10(10):1025-1031

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 07,1998
  • Revised:October 19,1998
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2035311Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063