System Level Design Methods for
Reactive Embedded Systems

Overview

Message Sequence Charts (MSC) have been traditionally used to depict execution scenarios in the early stages of design cycle. MSCs portray inter-process (inter-object) interaction and synthesizing intra-process (intra-object) executable specifications from an MSC-based description is a non-trivial task. The Communicating Transaction Processes (CTP) model is based on MSCs from which an executable specification can be extracted in a straightforward manner. Our CTP model describes a network of communicating processes as a collection of high-level labeled transition systems, where processes interact via common actions labels. Each action is, in general, a non-atomic interaction which is captured by a guarded choice of MSCs. Thus our model achieves a separation of concerns: the high-level transition system depict intra-process control flow and computations, while the non-atomic actions in the transition system depict inter-process interaction via MSCs. The model is under active development on notational, formal and experimental fronts.

The CTP model is intended to serve as Model of Computation (MOC) for use in the system-level design of embedded reactive systems. The way computations are seperated from communications and the fact it is based on UML notations makes it an attractive candidate also for providing a "standard" higher-level of abstraction for a language such as SystemC. Most of our current research is directed towards realizing these potential benefits of the model.

People

Faculty Members

• Abhik Roychoudhury
  e-mail: abhik@comp.nus.edu.sg
• Dong Jin Song
  e-mail: dongjs@comp.nus.edu.sg
• P.S. Thiagarajan
  e-mail: thiagu@comp.nus.edu.sg
• Samarjit Chakraborty
  e-mail:samarjit@comp.nus.edu.sg
• Wong Weng Fai
  e-mail:wongwf@comp.nus.edu.sg

Ph.D Students

• Ankit Goel
  ankitgoe@comp.nus.edu.sg
• CHEN Chunqing
  chenchun@comp.nus.edu.sg
• Kathy Nguyen Dang
  kathyngu@comp.nus.edu.sg
• Phan Thi Xuan Linh
  phanthix@comp.nus.edu.sg
• SUN Jun
  sunj@comp.nus.edu.sg
• Tran Tuan Anh
  trantuan@comp.nus.edu.sg
• Yang Shaofa
  yangsf@comp.nus.edu.sg

Honours Year Project(HYP) Students

• Gloria Teng Sze Ting
• Geoffrey Koh
• Koey Huishan
• Lee Wai See
• Loy Jen Yan
• Ng Lai Yin
• Peh Chern Liang
• Tan Wee Hon

Research Funding

Our research is being supported substantially by the Embedded and Hybrid Systems (EHS) programme of A*STAR (Agency for Science, Technology and Research), Singapore.

Title: Formal Design Techniques for Reactive Embedded Systems

Abstract: Embedded system design has become important in the recent years with the integration of microcomputers in in a wide range of commonly used applications. Many of these embedded systems are reactive (where the embedded computing component interacts with the physical environment in an ongoing fashion) and safety critical e.g. automotive applications. This project will concentrate on building formal design techniques with the following aims:

• Inject greater reliability in the design cycle by doing analysis and verification at early design stages.
• Contribute to the development of UML-compatible design methods to enhance applicability.
• Develop translation mechanisms for linking requirements to executable specifications.
• Develop translation mechanisms for linking executable specifications to a platform description language for code generation.
• Construct techniques for specifying and synthesizing communication interfaces to enable component-based design of complex reactive systems.

A key feature of our approach is the use of the appealing graphical notation called Message Sequence Charts at the executable specification level. A second important feature is the use of an integrated combination of state oriented (Object-Z) and process oriented (Timed CSP), mechanisms -called TCOZ- to capture the requirements concerning complex reactive embedded systems.

Relevant Publications

Papers

• Communicating Transaction Processes: An MSC-based Model of Computation for Reactive Embedded Systems (.pdf)
  A. Roychoudhury and P.S. Thiagarajan
  
• Synthesizable SystemC Code from UML models (.pdf)
  W.H. Tan, P.S. Thiagarajan, W.F. Wong, Y. Zhu and S.K. Pilakkat
  
• Lazy Rectangular Hybrid Automata (.pdf)
  M. Agrawal and P.S. Thiagarajan
  Proc. of 7th International Workshop on Hybrid Systems: Computation and Control, Springer lecture Notes in Computer Science 2003, To appear.
• A Theory of Regular MSC Languages (.pdf)
  J. G. Henriksen, M. Mukund, K. Narayan Kumar, M. Sohoni and P.S. Thiagarajan
  Information and Computation, To appear.
• Netcharts: Bridging the gap between HMSCs and executable specifications (.pdf)
  M. Mukund, K Narayan Kumar and P.S. Thiagarajan
  Proc. of the 14th International Conference on Concurrency Theory (CONCUR'03)}, Springer Lecture Notes in Computer Science 2761, Springer-Verlag, 2003.
• Communicating Transaction Processes (.ps)
  A. Roychoudhury and P.S. Thiagarajan
  IEEE International Conference on Application of Concurrency in System Design (ACSD) 2003, To appear.
• An Executable Specification Language based on Message Sequence Charts (.ps)
  A. Roychoudhury and P.S. Thiagarajan
  Formal Methods at the Crossroads: From Panacea to Foundational Support, Springer Lecture Notes in Computer Science, To appear.
• Message Sequence Charts (.ps)
  D. Harel, P.S. Thiagarajan
  In: UML for Real: Design of Real Time Embedded Systems, Eds.: Luciano Lavagno, Grant Martin, Bran Selic, Kluwer Academic Publishers, 2003.

Theses & Reports

• Analysis Methods for Cyclic Transaction Processes (.ps, .pdf)
  Tran Tuan Anh
  Honours year report, School of Computing National University of Singapore, 2003
• A Programming Paradigm for Modelling Reactive Embedded Systems (.ps)
  Prakash Chandrasekaran
  Master thesis, 2003