FIU Home
About CADSE
Research
Recent Publications
CADSE Activities
People
Opportunities
Training
Funding
Contact Info
Links



CADSE Home


List of Selected Publications from the Software Architecture research project:

  • Journals
    1. Jiacun Wang, MengChu Zhou and Yi Deng,"Modeling and Throughput Analysis of Discrete Event Systems Based on Stochastic Petri Nets", International Journal of Intelligent Control and Systems, Vol. 3, no.3, 343-358, 1999.


      2. Abstract:
      This paper presents an algorithm of polynomial complexity to derive the throughput of a discrete event system via stochastic Petri net (SPN) models. The concept of flow nets, a subclass of SPN, is introduced to model a class of discrete event systems. The mathematical model for the throughput of flow nets is given and analysis can be performed through linear programming. The linear programming problem size can be significantly reduced for a class of structurally non-competitive and acyclic flow nets. A procedure is proposed to convert a structurally competitive and cyclic flow net to a structurally non-competitive and acyclic one in the sense of equivalent throughput. A discrete manufacturing system is used to illustrate the application of the proposed concepts and algorithm for its throughput analysis.
    2. Yi Deng and Jiacun Wang, "Integrated Architectural Modeling and Analysis for High-Assurance Command and Control System Design", Annals of Software Engineering,Vol.7, 47-70, 1999.


      3. Abstract:
      In this paper, we introduce compositional time Petri net (CTPN) models. A CTPN is a modularized time Petri net (TPN), which is composed of components and connectors. We also propose a set of component-level reduction rules for TPN's. Each of these reduction rules transforms a TPN component to a constant size of simple one while maintains the net's external observable timing properties. Consequently, our method works at a coarser level than that works in individual transition level, and fewer applications of our rules are needed to reduce the size of the TPN under analysis. We illustrate the use and benefits of CTPN's and reduction rules by modeling and analyzing the response time of a command and control system to its external arriving messages.
    3. Jiacun Wang, Xudong He and Yi Deng, "Introducing Software Architecture Specification and Analysis in SAM through an Example", Information and Software Technology, Vol.41, No.7, 451-567, 1999.


      4. Abstract:
      Software architecture study has become one of the most active research areas in software engineering in recent years. Although there have been many published results on specification and analysis methods of software architectures, there is a lack of a sound systematic methodology for modeling and analyzing software architectures. In this paper, we present a formal systematic software architecture specification and analysis methodology called SAM. We show how to apply SAM to specify a command control (C2) system and to analyze its real-time constraints.
    4. Jiacun Wang and Yi Deng, "Incremental modeling and verification of flexible manufacturing systems", Journal of Intelligent Manufacturing, Vol. 10, No. 6, 1999.


      5. Abstract:
      An FMS is a typical real-time concurrent system composed of a number of computer-controlled machine tools, automated material handling and storage systems that operate as an integrated system under the control of host computer(s). The growing demand for higher performance and flexibility in these systems and the interlocking factors of concurrency, deadline-driven activities, and real-time decision making pose a significant challenge in FMS design, especially in terms of control and scheduling. A formal engineering approach that helps handle the complexity and dynamics of FMS modeling, design and analysis is needed. A Real-time Architectural Specification (RAS) model and its application in the modeling of flexible manufacturing system (FMS) are presented. RAS combines mature operational and descriptive formal methods, in particular Time Petri nets (TPN) and Real-Time Computational Tree Logic (RTCTL), to form an integrated system model for architectural specification and analysis of real-time concurrent systems such as FMS.

      Download (1.2Mb - PostScript format)
    5. Yi Deng, C. Yang, "Architecture-driven modeling of real-time concurrent systems with application in FMS", Journal of Systems and Software, Vol. 10, No. 6, pp.61-78, 1999.


    6. Y. Deng, S. K. Chang and X. Lin, "Executable specification and analysis for the design of concurrent object-oriented systems". International Journal of Software Engineering and Knowledge Engineering, 4(4):427-450, 1993.


    7. Dianxiang Xu, Guoliang Zheng and Xiaocong Fan, "A logic based language for networked agents", Information and Software Technology, Vol. 40, no. 8, 435-442, 1998.

    8. X. He and Y. Deng: "Specifying Software Architectural Connectors in SAM", International Journal of Software Engineering and Knowledge Engineering, vol.10, no.4, 2000, 411-431.

    9. X. He and Y. Deng: "A Framework for Developing and Analyzing Software Architecture Specifications in SAM", The Computer Journal, vol.45, no.1, 2002, 111-128.

    10. D. Xu, J. Yin, Y. Deng and J. Ding, "Architectural Modeling of Logical Agent Mobility", IEEE Transactions on Software Engineering, vol. 29, no. 1, 2003, 31 - 45.

    11. Y. Deng, J. Wang, K. Beznosov and J.P. Tsai, "An approach for modeling and analysis of security system architectures", IEEE Transactions on Knowledge and Data Engineering, vol. 15, no. 2, 2003.

    12. X. He, H. Yu, T. Shi, J. Ding, and Y. Deng: "Formally Analyzing Software Architectural Specifications Using SAM", Journal of Systems and Software, 2004 (in press).

  • Conferences
    1. Jiacun Wang, Chun Jin and Yi Deng, "Performance Analysis of Traffic Control System Based on Stochastic Timed Petri Net Models", Proceedings of the 23rd Annual International Computer Software and Applications Conference, Phoenix, Arizona, pp. 436-441, 1999.


      2. Abstract:
      We present a new modeling method to evaluate the performance indices of traffic control systems where each intersection has two or four phases. The method is based on the stochastic timed Petri net models of isolated intersections. It considers one direction of traffic along a street each time, and the interactions between traffic of different directions are partially approximated by statistical models. By so doing, it dramatically reduces the computing complexity that other Petri net-based methods suffer due to the consideration of detailed interactions among all directions of traffic. An example is presented to show the potential application of the new method.
    2. Xudong He, Fancong Zeng and Yi Deng, "Specifying Software Architectural Connectors in SAM", Proceedings of the 11th International Conference on Software Engineering and Knowledge Engineering, Germany, June 1999.


      3. Abstract:
      Software architecture has become one of the most active research topics in software engineering in recent years. One of the distinct features of software architecture research is to explicitly study the interconnections (connectors) among system components. In this paper, we show how to formally specify several well-known general connectors in a software architecture methodology called SAM. Related work is discussed and compared. Our results establish the basis for reusing these defined connectors and for building more sophisticated connectors from them.
    3. Jiacun Wang, Chun Jin and Yi Deng, "Performance Analysis of Traffic Networks Based on Stochastic Timed Petri Net Models", Proceedings of the 5th IEEE International Conference on Engineering of Complex Computer Systems, Las Vegas, pp.77-85, 1999.


      4. Abstract:
      A compositional method for modeling and evaluation of performance indices of traffic control systems based on Stochastic Timed Petri Nets (STPN) is presented. We use STPN to specify traffic and traffic control at an intersection and use a random distribution model to model the motion of vehicles in a road segment between any two consecutive intersections. The traffic control system is thus modeled as a composition of individual intersection models and segment distribution models. A technique is presented to incrementally evaluate the system's performance by analyzing intersections separately according to a carefully selected order. The analysis technique conforms to the accepted practice of transportation research. Compared to existing Petri net models of traffic control systems, our technique dramatically reduces the complexity of analysis.
    4. Yi Deng, Jiacun Wang, and Rakesh Sinha, "Integrated architecture modeling of real-time concurrent systems with applications in FMS", Proceedings of the 10th International Conference on Software Engineering and Knowledge Engineering, San Francisco Bay, pp. 34-43, June 1998.


      5. Abstract:
      A Real-time Architectural Specification (RAS) model and its application in the modeling of flexible manufacturing system (FMS) are presented. An FMS is a typical real-time concurrent system. The growing demand for higher performance and flexibility in these systems and the interlocking factors of concurrency, deadline-driven activities, and real-time decision making pose a significant challenge in FMS design, especially in terms of control and scheduling. A formal engineering approach that helps handle the complexity and dynamics of FMS modeling, design and analysis is needed. RAS combines mature Time Petri nets and Real-Time Computational Tree Logic to form an integrated system model for architectural specification and analysis of real-time concurrent systems such as FMS.

      Download (799k - PostScript format)
    5. Yi Deng, Jiacun Wang, and Rakesh Sinha, "Incremental Architectural Modeling and Verification of Real Time Concurrent systems", Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods, Brisbane, Australia, pp. 26-34, December 1998.


      6. Abstract:
      An incremental approach for architectural modeling and analysis of real-time concurrent systems is presented. The approach integrates existing formal methods, more specifically time Petri nets and real-time computational tree logic, and leverages their complementary strengths in a way that allows us to systematically link and enforce that architectural design meets the system's timing requirements, and to incrementally verify the conformance. Consequently, our approach is able to provide better assurance to system design and yet reduce the complexity of analysis. Our approach is based on a Real-time Architectural Specification (RAS) model, which provides a formal basis to systematically maintain a correlation between the (timing) requirements of a system and its architectural design. Based on RAS, we further present a method to verify timing properties of a system design. This method helps conquer the complexity of analysis in two dimensions. Horizontally at each design level, incremental verification is achieved by introducing TPN reduction rules that allow us to compose analysis results on individual system components. Vertically across design levels, incremental verification is achieved by propagating higher-level constraints to lower-level designs so that we can safely plug a component design into a high-level architecture without having to re-verify the entire model. A naval command and control (C2) system is used throughout the paper to demonstrate the concept and usability of our approach.

      Download (731k - PostScript format)
    6. Jiacun Wang and Yi Deng, "Component-level reduction rules for time Petri nets with application in C2 systems", Proceedings of the IEEE Conference on System, Man and Cybernetics, San Diego, California, pp. 125-130, October 1998.


      7. Abstract:
      In this paper, we propose a set of component-level reduction rules for TPN's. Each of these reduction rules transforms a TPN component to a constant size of simple one while maintains the net's external observable timing properties. Consequently, our method works at a coarser level than that works in individual transition level, and fewer applications of our rules are needed to reduce the size of the TPN under analysis. We illustrate the use and benefits of our reduction rules by modeling and analyzing the response time of a command and control system to its external arriving messages.

      Download (556k - PostScript format)
    7. Yi Deng and Jiacun Wang, "Integrated architectural modeling and analysis for high-assurance command and control system design", Proceedings of 3rd IEEE High-Assurance System Engineering Symposium, Washington, pp.270-278, 1998.


      8. Abstract:
      A Real-Time Architectural Specification (RAS) model and its application to command and control (C2) systems are presented. The objective is to establish a formal foundation that will enable us to integrate existing rich but fragmented formal techniques for system specification and verification into practical and scaleable formal engineering methods to support the design and development of highly reliable real-time distributed systems. Based on RAS models, we further present an incremental method for verifying timing properties of a RAS model that helps to reduce the complexity of analysis both at a given design level or across different design levels.

      Download (718k - PostScript format)
    8. Jiacun Wang, Yi Deng and Xudong He, "A formal architectural specification model for real-time systems design", Proceedings of IASTED Conference on Software Engineering, Las Vegas, pp. 11-14, 1998.


      9. Abstract:
      In this paper, a Real-time Architectural Specification (RAS) model is presented. The objective of RAS is to establish a formal foundation that will enable us to integrate existing rich but fragmented formal techniques for system specification and verification into practical and scaleable formal engineering methods to support the design and development of highly reliable real-time distributed systems. The contribution of RAS is twofold: First, it offers an incremental and more scaleable approach for design modeling. Second, it provides a systematic way to enforce and maintain the consistency of the real-time system constraints in every step of the design process. These two features together make RAS a suitable model for the design of real-time systems.

      Download (338k - PostScript format)
    9. Yi Deng, S. Lu and M. Evangelist. "A formal approach for specification and prototyping of real-time distributed systems". Proceedings of Hawaii International Conference on Sytem Science, 1997.


    10. Y. Deng, W. Du, P. C. Attie and M. Evangelist. "A formal approach for architectural modeling and decomposition of distributed real-time systems". Proceedings of 8th International Conference on Software Engineering and Knowledge Engineering, Nevada, 408-417, 1996.


    11. Y. Deng, S. K. Chang, J. Figueiredo and A. Perkusich. "Integrating software engineering methods and Petri nets for the specification and prototyping of complex information systems". Proceedings of the 14th International Conference on Application and Theory of Petri Nets, Lecture Notes in Computer Science, 691, 207-223, 1993.


    12. Y. Deng, R. K. Ege and W. Sun. "Executable specifications for the design of object-orinted systems". Proceedings of 5th International Conference on Software Engineering and Knowledge Engineering, 16-18, San Francisco, 1993.


    13. X. Liu, Y. Deng, and X. He: "Development of A Distributed Time Petri Net Simulator in the SAM Framework", Proc. of the Symp. On Performance Evaluation of Computer and Telecommunication Systems, Orlando, 2001, 223-230.

    14. T. Shi and X. He: "Modeling and Analyzing the Software Architecture of A Communication Protocol Using SAM", Software Architecture- System Design, Development and Maintenance (eds. J. Bosch, M. Gentleman, C. Hofmeister, and J. Kuusela), Kluwer Academic Publishers, 2002, 63-78.

    15. H. Reza and X. He: "Petri Net Patterns: Elements of Reusable Petri Net Specifications", Proc. of the 2002 International Conference on Software Engineering Research and Practice, Las Vegas, July, 2002, 173-179.

    16. X. He, J. Ding, and Y. Deng: "Analyzing SAM Architectural Specifications Using Model Checking", Proc. of SEKE2002, Italy, 2002, 271-274.

    17. H. Yu, X. He, Y. Deng, and L. Mo: "A Formal Method for Analyzing Software Architecture Models in SAM", Proc. of COMPSAC2002, Oxford, U.K., 2002, 645-652.

    18. H. Yu, X. He, Y. Deng, and L. Mo: "Formal Analysis of Real-Time Systems with SAM", Proc. of the 4th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, vol.2495, October, Shanghai, China, 2002, 275-286.

    19. H. Yu, X. He, , S. Gao and Y. Deng: "Modeling and Analyzing SMIL Documents in SAM", Proc. of MSE2002, Newport Beach, California, Dec. 2002, 132-139.

    20. T. Shi and X. He: "A Methodology for Dependability and Performability Analysis In SAM", Proc. of The International Conference on Dependable Systems and Networks, San Francisco, CA, June 2003, 679-688.

    21. T. Shi and X. He: "Dependeability Analysis using SAM", Proc. of the ICSE Workshop on Software Architectures for Dependable Systems, May 3, Portland, Oregon, USA, 2003, 37-42.

    22. H. Reza and X. He: "Pattern-Based Software Architecture: A Case Study", Proc. of the IEEE International Conference on Information Technology: Coding and Computing, Las Vegas, 2003, 592-597.

    23. H. Yu, X. He, S. Gao, and Y. Deng: "Formal Software Architecture Design of Secure Distributed Systems", Proc. of SEKE 2003, California, 2003, 450-457.

    24. H. Reza and X. He: "An Integrated Method to Software Architecture", Proc. of SEKE 2003, CA, 2003, 398-405.

  • Technical Reports
    1. Yi Deng, Dianxiang Xu and Junhua Ding, "Architectural modeling of mobile agents", Technical Report. FIU-CS-CADSE, December 1999.

    2. Yi Deng, Junhua Ding and Dianxiang Xu, "Formalizing MASIF interoperable architecture of mobile agent systems", Technical Report. FIU-CS-CADSE, December 1999.
[ Software Architecture Home ]

For problems or questions about this web, contact webmaster@cadse.cs.fiu.edu