This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance
September 2005 (vol. 31 no. 9)
pp. 713-732
ASCII Text
x 
 
Dongfeng Wang, Farokh B. Bastani, I.-Ling Yen, "Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance," IEEE Transactions on Software Engineering, vol. 31, no. 9, pp. 713-732, September, 2005.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2005.99,
author = {Dongfeng Wang and Farokh B. Bastani and I.-Ling Yen},
title = {Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance},
journal ={IEEE Transactions on Software Engineering},
volume = {31},
number = {9},
issn = {0098-5589},
year = {2005},
pages = {713-732},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2005.99},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance
IS - 9
SN - 0098-5589
SP713
EP732
EPD - 713-732
A1 - Dongfeng Wang,
A1 - Farokh B. Bastani,
A1 - I.-Ling Yen,
PY - 2005
KW - Index Terms- Software decomposition
KW - dependability assurance
KW - process-control systems
KW - aspect-oriented modeling.
VL - 31
JA - IEEE Transactions on Software Engineering
ER -
 
This paper presents a method for decomposing process-control systems. This decomposition method is automated, meaning that a series of principles that can be evolved to support automated tools are given to help a designer decompose complex systems into a collection of simpler components. Each component resulting from the decomposition process can be designed and implemented independently of the other components. Also, these components can be tested or verified by the end-user independently of each other. Moreover, the system properties, such as safety, stability, and reliability, can be mathematically inferred from the properties of the individual components. These components are referred to as IDEAL (Independently Developable End-user Assessable Logical) components. This decomposition method is applied to a case study specified by the High-Integrity Systems group at Sandia National Labs, which involves the control of a future version of the Bay Area Rapid Transit (BART) system.

[1] E.A. Emerson and J.Y. Halpern, “‘Sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time Temporal Logic,” J. ACM, vol. 33, no. 1, pp. 151-178, Jan. 1986.
[2] J. Araújo, J. Whittle, and D.-K. Kim, “Modeling and Composing Scenario-Based Requirements with Aspects,” Proc. 12th IEEE Int'l Requirements Eng. Conf., pp. 58-67, Sept. 2004.
[3] J.M. Atlee and J. Gannon, “State-Based Model Checking of Event-Driven System Requirements,” IEEE Trans. Software Eng., vol. 19, no. 1, pp. 24-40, Jan. 1993.
[4] F.B. Bastani, “Relational Programs: An Architecture for Robust Real-Time Safety-Critical Process-Control Systems,” Annals of Software Eng., vol. 7, pp. 5-24, 1999.
[5] F.B. Bastani, V.L. Winter, and I.-L. Yen, “Dependability of Relational Safety-Critical Programs,” Proc. IEEE Int'l Symp. Software Reliability Eng., Nov. 1999.
[6] F.B. Bastani, I.-L. Yen, and S. Kim, “Highly Reliable Relational Control Programs for Robust Rapid Transit Systems,” Proc. Sixth IEEE Int'l Symp. High Assurance Systems Eng. (HASE 2001), pp. 65-74, Oct. 2001.
[7] F.B. Bastani, I.-L. Yen, S. Kim, J. Linn, and K. Rao, “Reliability of Systems of Independently Developable End-User Assessable Logical (IDEAL) Programs,” The 12th Int'l Symp. Software Reliability Eng., pp. 314-323, Nov. 2001.
[8] D. Batory, J.N. Sarvela, and A. Rauschmayer, ”Scaling Step-Wise Refinement,” IEEE Trans. Software Eng., vol. 30, no. 6, pp. 355-371, June 2004.
[9] B.B. Bista, K. Takahashi, and N. Shiratori, “Composition of Service and Protocol Specifications,” Proc. Int'l Conf. Information Networking (ICOIN), pp. 171-178, Jan. 2001.
[10] E.D. Brinksma and R. Langerak, “Functionality Decomposition by Compositional Correctness Preserving Transformation,” Computer Aided Verification (CAV), pp. 371-384, 1993.
[11] J.R. Burch, E.M. Clarke, and D.E. Long, “Symbolic Model Checking with Partitioned Transition Relations,” Proc. Int'l Conf. Very Large Scale Integration, 1990.
[12] S.V. Campos, “A Quantitative Approach to the Formal Verification of Real-Time System,” PhD thesis, SCS, Carnegie Mellon Univ., 1996.
[13] W. Chan, R.J. Anderson, and D. Notkin, “Model Checking Large Software Specifications,” IEEE Trans. Software Eng., vol. 24, no. 7, pp. 498-520, July 1998.
[14] S. Clarke, “Extending Standard UML with Model Composition Semantics,” Science of Computer Programming, vol. 44, no. 1, pp. 71-100, May 2002.
[15] S. Clarke, W. Harrison, H. Ossher, and P. Tarr, “Subject-Oriented Design: Toward Improved Alignment of Requirements, Design, and Code,” Proc. Conf. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 325-339, Nov. 1999.
[16] S. Clarke and R.J. Walker, “Composition Patterns: An Approach to Designing Reusable Aspects,” Proc. Int'l Conf. Software Eng. (ICSE), pp. 5-14, May 2001.
[17] J.B. Dugan and R. VanBuren, “Reliability Evaluation of Fly-by-Wire Computer Systems,” J. of Systems and Safety, June 1993.
[18] R.E. Filman, S. Barrett, D.D. Lee, and T. Linden, “Inserting Ilities by Controlling Communications,” Aspect-Oriented Software Development, R.E. Filman et al., eds., pp. 283-296, 2005.
[19] O. Grumberg and D. Long, “Model Checking and Modular Verification,” ACM Trans. Programming Languages and Systems, vol. 16, no. 3, pp. 843-871, May 1994.
[20] J. Jezequel, N. Plouzeau, T. Weis, and K. Geihs, “From Contracts to Aspects in UML Designs,” Proc. Workshop Aspect-Oriented Modeling with UML at AOSD, 2002.
[21] G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W.G. Griswold, “An Overview of AspectJ,” Proc. European Conf. Object-Oriented Programming, pp. 327-353, June 2001.
[22] G. Kiczales, J. Lamping, and A. Mendhekar, “Aspect-Oriented Programming,” Proc. European Conf. Object-Oriented Programming (ECOOP), pp. 220-242, June 1997.
[23] S. Kim, F.B. Bastani, I.-L. Yen, and I.-R. Chen, “Systematic Reliability Analysis of a Class of Application-Specific Embedded Software Frameworks,” IEEE Trans. Software Eng., vol. 30, no. 4, pp. 218-230, Apr. 2004.
[24] S.S. Lam and A.U. Shankar, “Protocol Verification via Projections,” IEEE Trans. Software Eng., vol. 10, no. 4, pp. 325-342, July 1984.
[25] S.S. Lam and A.U. Shankar, “A Theory of Interfaces and Modules I-Composition Theorem,” IEEE Trans. Software Eng., vol. 20, no. 1, pp. 57-71, Jan. 1994.
[26] L. Lamport, ”The Temporal Logic of Actions,” ACM Trans. Programming Languages and Systems, vol. 16, no. 3, pp. 872-923, May 1994.
[27] N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, “Requirements Specification for Process-Control Systems,” IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[28] H.-A. Ling, “Constructing Protocols with Alternative Functions,” IEEE Trans. Computers, vol. 40, no. 4, pp. 376-386, Apr. 1991.
[29] H.-A. Ling and C.-L. Tarng, “An Improved Method for Constructing Multiphase Communications Protocols,” IEEE Trans. Computers, vol. 42, no. 1, pp. 15-26, Jan. 1993.
[30] A. Mendhekar, G. Kiczales, and J. Lamping, “Rg: A Case-Study for Aspect-Oriented Programming,” Technical Report SPL97-009 P9710044, Xerox PARC, Palo Alto, Calif., Feb. 1997.
[31] S. Morasca, A. Morzenti, and P. Sanpietro, “Generating Functional Test Cases In-the-Large for Time-Critical Systems from Logic-Based Specifications,” Proc. 1996 ACM SIGSOFT Int'l Symp. Software Testing and Analysis, vol. 21, no. 3, May 1996.
[32] S. Narain and J. Rothenberg, “Proving Temporal Properties of Hybrid Systems,” Proc. 22nd Conf. Winter Simulation, Dec. 1990.
[33] H. Ossher and P. Tarr, “Hyper/J: Multi-Dimensional Separation of Concerns for Java,” Proc. Int'l Conf. Software Eng., pp. 729-730, 2001.
[34] D.L. Parnas, “On the Criteria to be Used in Decomposing Systems into Modules,” Comm. ACM, vol. 15, no. 12, pp. 1053-1058, Dec. 1972.
[35] A. Pnueli, “The Temporal Logic of Concurrent Programs,” Theoretical Computer Science, vol. 13, pp. 45-60, 1981.
[36] N. Rescher and A. Urquhart, Temporal Logic. Springer-Verlag, 1971.
[37] K.D. Shere and R.A. Carlson, “A Methodology for Design, Test, and Evaluation of Real-Time Systems,” Computer, vol. 27, no. 2, pp. 35-48, Feb. 1994.
[38] G. Singh, “A Compositional Approach for Designing Protocols,” Proc. Int'l Conf. Network Protocols, pp. 98-105, Oct. 1993.
[39] B. Steffen, S. Graf, and G. Lüttgen, “Compositional Minimization of Finite State Systems,” Int'l J. Formal Aspects of Computing, vol. 8, pp. 607-616, 1996.
[40] A.H. Thomas, M. Minea, and V. Prabhu, “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems,” Proc. Fourth Int'l Workshop Hybrid Systems: Computation and Control, pp. 275-290, Mar. 2001.
[41] C. Toinard, G. Florin, and C. Carrez, “A Formal Method to Prove Ordering Properties of Multicast Systems,” ACM SIGOPS Operating Systems Rev., vol. 33, no. 4 Oct. 1999.
[42] D.F. Wang, F.B. Bastani, I-L. Yen, and R. Paul, “An Approach for Designing Highly Adaptable Process-Control Systems,” Proc. Eighth IEEE Int'l Symp. Object-Oriented Real-Time Distributed Computing, Mar. 2005.
[43] D.F. Wang, P. Jain, F.B. Bastani, and I-L. Yen, “Stepwise Development of High-Assurance Process-Control Systems Based on Independently Developable End-User Assessable Logical (IDEAL) Aspects,” Technical Report, Dept. of Computer Science, UT-Dallas, www.utdallas.edudongfeng.wang/, Apr. 2005.
[44] V. Winter, R. Berg, and J. Ringland, “Bay Area Rapid Transit District Advanced Automated Train Control System Case Study Description,” Sandia Nat'l Labs, 1999.
[45] Y. Yu, J.C. SampaiodoPradoLeite, and J. Mylopoulos, “From Goals to Aspects: Discovering Aspects from Requirements Goal Models,” Proc. 12th IEEE Int'l Requirements Eng. Conf., pp. 38-47, Sept. 2004.
[46] P. Zave, “A Distributed Alternative to Finite-State-Machine Specifications,” ACM Trans. Programming Language and System, vol. 7, no. 1, pp. 10-36, Jan. 1985.

Index Terms:
Index Terms- Software decomposition, dependability assurance, process-control systems, aspect-oriented modeling.
Citation:
Dongfeng Wang, Farokh B. Bastani, I.-Ling Yen, "Automated Aspect-Oriented Decomposition of Process-Control Systems for Ultra-High Dependability Assurance," IEEE Transactions on Software Engineering, vol. 31, no. 9, pp. 713-732, Sept. 2005, doi:10.1109/TSE.2005.99
Usage of this product signifies your acceptance of the Terms of Use.