III/1 UNU/IIST Reports

 [397]
Kamel Boumaza, J.W. Sanders, and Wang Xu. Timing models for asynchronous circuits. Research Report 397, UNU-IIST, P.O.Box 3058, Macau, May 2008. abstract pdf

 [396]
Miaomiao Zhang, Dang Van Hung, and Zhiming Liu. Verification of Linear Duration Invariants by Model Checking CTL Properties. Research Report 396, UNU-IIST, P.O.Box 3058, Macau, June 2008. abstract pdf

 [395]
Abigail Parisaca Vargas and Chris George. Formalising the translation from RSL to CSP. Research Report 395, UNU-IIST, P.O.Box 3058, Macau, May 2008. abstract pdf

 [394]
J.W. Sanders. On Research: Incremental Semantics. Research Report 394, UNU-IIST, P.O.Box 3058, Macau, May 2008. abstract pdf

 [393]
Lizeth Tapia and Chris George. Model Checking Concurrent RSL with CSPM and FDR2. Research Report 393, UNU-IIST, P.O.Box 3058, Macau, April 2008

 [392]
Mike Reed, Chris George, and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2007. Administrative Report 392, UNU-IIST, P.O.Box 3058, Macau, April 2008. abstract pdf

 [391]
I.M. Rewitzky and J.W.Sanders. Involutions on Relational Program Calculi. Research Report 391, UNU-IIST, P.O.Box 3058, Macau, February 2008. abstract pdf

 [390]
Hu Jun, Zhiming Liu, G. M. Reed, and J. W. Sanders. Position Paper: Ensemble Engineering and Emergence (and Ethics?). Research Report 390, UNU-IIST, P.O.Box 3058, Macau, December 2007. abstract pdf

 [389]
Lu Yang, Volker Stolz, and Zhiming Liu. Integrating Refinement into Software Development Tools. Research Report 389, UNU-IIST, P.O.Box 3058, Macau, November 2007. abstract pdf

 [388]
Zhenbang Chen, Zhiming Liu, Anders P. Ravn, Volker Stolz, and Naijun Zhan. Refinement and Verification in Component-Based Model Driven Design. Research Report 388, UNU-IIST, P.O.Box 3058, Macau, November 2007. abstract pdf

 [387]
Miaomioa Zhang, Zhiming Liu, and Anders P. Ravn. Design and Verification of a Fault-Tolerant System. Research Report 387, UNU-IIST, P.O.Box 3058, Macau, November 2007. abstract pdf

 [386]
Abdel Hakim Hannousse and Zhiming Liu. Towards a Calculus for Design Patterns. Research Report 386, UNU-IIST, P.O.Box 3058, Macau, October 2007. abstract pdf

 [385]
Volker Stolz and Geguang Pu, editors. Proceedings of the 1st International Workshop on Harnessing Theories for Tool Support in Software TTSS'07, 22-23 September 2007, Macau SAR, China, number 385 in UNU-IIST Reports, P.O.Box 3058, Macau, September 2007 pdf

 [384]
Dimitar P. Guelev and Dang Van Hung. Reasoning about QoS Contracts in the Probabilistic Duration Calculus. Research Report 384, UNU-IIST, P.O.Box 3058, Macau, September 2007. abstract pdf

 [383]
Zhenbang Chen, Xiaoshan Li, Zhiming Liu, and Volker Stolz. Harnessing rCOS for Tool Support: The CoCoMe Experience. Research Report 383, UNU-IIST, P.O.Box 3058, Macau, September 2007. abstract pdf

 [382]
Zhenbang Chen, Abdel Hakim Hannousse, Dang Van Hung, Istvan Knoll, Xiaoshan Li, Zhiming Liu, Yang Liu, Qu Nan, Joseph C. Okika, Anders P. Ravn, Volker Stolz, Lu Yang, and Naijun Zhan. Modelling with Relational Calculus of Object and Component Systems - rCOS. Research Report 382, UNU-IIST, P.O.Box 3058, Macau, September 2007. abstract pdf

 [381]
Liang Zhao, Xiaojian Liu, Zhiming Liu, and Zongyan Qiu. Graph Transformations for Object-Oriented Refinement. Research Report 381, UNU-IIST, P.O.Box 3058, Macau, September 2007. abstract pdf

 [380]
J W Sanders. Behaviour Approximated on Subgroups. Research Report 380, UNU-IIST, P.O.Box 3058, Macau, September 2007. abstract pdf

 [379]
Yifeng Chen and J W Sanders. A Pointer Logic for Object Diagrams. Research Report 379, UNU-IIST, P.O.Box 3058, Macau, July 2007. abstract pdf

 [378]
Chris George, Padmanabhan Krishnan, P A P Salas, and J W Sanders. Specification for Testing. Research Report 378, UNU-IIST, P.O.Box 3058, Macau, July 2007. abstract pdf

 [377]
Dang Van Hung. Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus. Research Report 377, UNU-IIST, P.O.Box 3058, Macau, June 2007. Published in LNCS 4700, Springer, 2007, pp. 170-187. abstract pdf

 [376]
Li Xiaolei and J W Sanders. Asynchronous Controller Design. Research Report 376, UNU-IIST, P.O.Box 3058, Macau, May 2007. abstract pdf

 [375]
Choe Changil and Dang Van Hung. On Verification of Linear Occurrence Properties of Real-Time Systems. Research Report 375, UNU-IIST, P.O.Box 3058, Macau, May 2007. abstract pdf

 [374]
Jong Hyo Jin and Chris George. Specifying and Verifying Multicast Communication Protocols. Technical Report 374, UNU-IIST, P.O.Box 3058, Macau, May 2007. abstract pdf

 [373]
G M Reed and J W Sanders. An Ethical Principle for Ubiquitous Communication. Technical Report 373, UNU-IIST, P.O.Box 3058, Macau, May 2007. abstract pdf

 [372]
Li Xiaolei and J W Sanders. Quadgate forward-signalling pipelines. Technical Report 372, UNU-IIST, P.O.Box 3058, Macau, April 2007. abstract pdf

 [371]
Adegboyega Ojo, Rilwan Basanya, Tomasz Janowski, and Mike Reed. South-South Cooperation in Software Technology. Technical Report 371, UNU-IIST, P.O.Box 3058, Macau, April 2007. Written for UNDP Special Unit on South-South Cooperation, to be part of the South Report. abstract pdf

 [370]
Adegboyega Ojo, Tomasz Janowski, and Elsa Estevez. A Composite Domain Framework for Developing Electronic Public Services. Technical Report 370, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the International Conference on Software Engineering Theory and Practice (SETP-07), Orlando, USA, July 2007. abstract pdf

 [369]
Adegboyega Ojo, Tomasz Janowski, and Elsa Estevez. Domain Models and Enterprise Application Framework for Developing Electronic Public Services. Research Report 369, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 6th International EGOV Conference 2007, Regensburg, Germany, September 2007, Trauner Druck. abstract pdf

 [368]
Elsa Estevez and Tomasz Janowski. Building a Dependable Messaging Infrastructure for Electronic Government. Technical Report 368, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 2nd International Workshop on Dependability and Security in e-Government (DeSeGov 2007), part of the International Conference on Availability, Reliability and Security, Vienna, Austria, April 2007, IEEE Computer Society. abstract pdf

 [367]
Elsa Estevez and Tomasz Janowski. Government-Enterprise Ecosystem Gateway (G-EEG) for Seamless e-Government . Research Report 367, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 40th Hawaii International Conference on System Sciences, Hawaii, January 2007, IEEE Computer Society. abstract pdf

 [366]
Maria Clara Casalini, Elsa Estevez, and Tomasz Janowski. Computing Support for Problem Solving in Virtual Communities of Practice. Technical Report 366, UNU-IIST, P.O.Box 3058, Macau, April 2007. Journal of Computer Science and Technology. Special Issue on Selected Papers from CACIC 2006, Vol. 7, No. 1, March 2007. abstract pdf

 [365]
Olumide Oteniya, Tomasz Janowski, and Adegboyega Ojo. Government-Wide Workflow Infrastructure - Enabling Virtual Government Organizations . Technical Report 365, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 7th IFIP Working Conference on Virtual Enterprises, Helsinki, Finland, September 2006, Springer-Verlag. abstract pdf

 [364]
Maria Clara Casalini, Tomasz Janowski, and Elsa Estevez. A Process Model for Collaborative Problem Solving in Virtual Communities of Practice. Research Report 364, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 7th IFIP Working Conference on Virtual Enterprises, Helsinki, Finland, September 2006, Springer-Verlag. abstract pdf

 [363]
Elsa Estevez, Tomasz Janowski, Adegboyega Ojo, and Irshad Kamal Khan. Coordination Offices for e-Government. Technical Report 363, UNU-IIST, P.O.Box 3058, Macau, April 2007. abstract pdf

 [362]
Adegboyega Ojo, Tomasz Janowski, Elsa Estevez, and Irshad Kamal Khan. Human Capacity Development for e-Government. Technical Report 362, UNU-IIST, P.O.Box 3058, Macau, April 2007. abstract pdf

 [361]
Elsa Estevez, Tomasz Janowski, and Adegboyega Ojo. Planning for e-Government - A Service-Oriented Agency Survey . Technical Report 361, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the IADIS International Conference on e-Society, Qawra, Malta, June 2005, IADIS. abstract pdf

 [360]
Adegboyega Ojo, Tomasz Janowski, and Elsa Estevez. Determining Progress Towards e-Government - What are the Core Indicators? . Research Report 360, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 5th European Conference on e-Government (ECEG 2005), Anterwerp, Belgium, June 2005, ACI. abstract pdf

 [359]
Tomasz Janowski, Elsa Estevez, and Adegboyega Ojo. A Project Framework for e-Government. Technical Report 359, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 4th International Conference on E-Government (EGOV05), Copenhagen, Denmark, August 2005, Trauner Druck. abstract pdf

 [358]
Tomasz Janowski, Elsa Estevez, and Adegboyega Ojo. The UNeGov.net Project - Building a Community of Practice for Electronic Governance. Administrative Report 358, UNU-IIST, P.O.Box 3058, Macau, April 2007. Invited talk at Digital Government 2006, Singapore, October 2006. Paper and poster presented and published in the proceedings of the 7th International Conference on Digital Government Research in San Diego, May 2006. abstract

 [357]
Tomasz Janowski, Adegboyega Ojo, and Elsa Estevez. The e-Macao Project - Building a Foundation for Electronic Government in Macao. Administrative Report 357, UNU-IIST, P.O.Box 3058, Macau, April 2007. Invited talk at the Hong Kong, Guangzhou and Macao Science and Industry Development Forum (Digital City), Guangzhou, China, September 2006. Invited talk at the African e-Government Forum, Accra, Ghana, March 2007. abstract

 [356]
Tomasz Janowski. Center for Electronic Governance at UNU-IIST. Administrative Report 356, UNU-IIST, P.O.Box 3058, Macau, April 2007. abstract

 [355]
Tran Thi Bich Hanh and Dang Van Hung. Verification of an Air-Traffic Control System with Probabilistic Real-time Model-checking. Technical Report 355, UNU-IIST, P.O.Box 3058, Macau, April 2007. abstract pdf

 [354]
Dang Van Hung and Pham Hong Thai. Towards a Template Language for Component-Based Programming. Technical Report 354, UNU-IIST, P.O.Box 3058, Macau, April 2007. Presented at and published in the proceedings of the 2007 International Conference on Software Engineering Research and Practice, SERP'07, Las Vegas, USA, June 25-28, 2007. abstract pdf

 [353]
Jeff W Sanders and Matteo Turilli. Dynamics of Control. Technical Report 353, UNU-IIST, P.O.Box 3058, Macau, March 2007. abstract pdf

 [352]
Chris George and Anne E. Haxthausen. Specification, Proof, and Model Checking of the Mondex Electronic Purse using RAISE. Technical Report 352, UNU-IIST, P.O.Box 3058, Macau, February 2007. abstract pdf

 [351]
Mike Reed, Chris George, and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2006. Administrative Report 351, UNU-IIST, P.O.Box 3058, Macau, February 2007. abstract pdf

 [350]
Xin Chen, He Jifeng, Zhiming Liu, and Naijun Zhan. A Model of Component-Based Programming. Technical Report 350, UNU-IIST, P.O.Box 3058, Macau, November 2006. Accepted by IPM International Symposium on Fundamentals of Software Engineering, April 17-19 2007, Tehran, Iran. abstract pdf

 [349]
Dang Van Hung, Alice Pun, and Chris George. Report on 2006 Survey of UNU-IIST Former Fellows. Administrative Report 349, UNU-IIST, P.O.Box 3058, Macau, November 2006. abstract pdf

 [348]
Chen Xin, Zhiming Liu, and Mike Reed, editors. Proceedings of 1st Asian Working Conference on Verified Software, AWCVS'06, number 348 in UNU-IIST Reports, P.O.Box 3058, Macau, November 2006. abstract pdf

 [347]
Antonio Cerone and Paul Curzon, editors. Proceedings of International Workshop Formal Methods for Interactive Systems FMIS 2006, number 347 in UNU-IIST Reports, P.O.Box 3058, Macau, November 2006. abstract pdf

 [346]
Bernhard Aichernig, Eerke Boiten, John Derrick, and Lindsay Groves, editors. Proceedings of International Refinement Workshop Refine 2006, number 346 in UNU-IIST Reports, P.O.Box 3058, Macau, November 2006. abstract

 [345]
Liang Zhao, Xiangpeng Zhao, Quan Long, and Zongyan Qiu. A Type System for the Relational Calculus of Object Systems. Technical Report 345, UNU-IIST, P.O.Box 3058, Macau, September 2006. abstract pdf

 [344]
Frank S. de Boer and Vladimir Mencl, editors. Preliminary Proceedings of the Third International Workshop on Formal Aspects of Component Software FACS'06, Prague, Czech Republic September 20-22, 2006, number 344 in UNU-IIST Reports, P.O.Box 3058, Macau, September 2006. abstract pdf

 [343]
Zhiming Liu, Vladimir Mencl, Anders P. Ravn, and Lu Yang. Harnessing Theories for Tool Support. Technical Report 343, UNU-IIST, P.O.Box 3058, Macau, August 2006. abstract pdf

 [342]
Norzima Elbegbayan. Reflection on Shared Experiences - Case Study on a Conference Support Website. Technical Report 342, UNU-IIST, P.O.Box 3058, Macau, August 2006. abstract pdf

 [341]
Hung Ledang and Dang Van Hung. Concurrency and Schedulability Analysis in Component-based Real-Time System Development. Technical Report 341, UNU-IIST, P.O.Box 3058, Macau, July 2006. Presented at and published in the proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering June 6 - 8, 2007 Shanghai, China. abstract pdf

 [340]
Xiaojian Liu, Zhiming Liu, and Liang Zhao. Object-Oriented Structure Refinement - A Graph Transformational Approach. Technical Report 340, UNU-IIST, P.O.Box 3058, Macau, July 2006. abstract pdf

 [339]
Joseph C. Okika, Zhiming Liu, and Anders P. Ravn. Analysis and Characterisation of a TTCN-3 Test System. Technical Report 339, UNU-IIST, P.O.Box 3058, Macau, June 2006. abstract pdf

 [338]
Jo Kwon Sik and Chris George. Specifying a Reliable Banking System in RSL. Technical Report 338, UNU-IIST, P.O.Box 3058, Macau, June 2006. abstract pdf

 [337]
Choe Chang Il and Dang Van Hung. Model Checking Durational Probabilistic Systems against Probabilistic Linear Duration Invariants. Technical Report 337, UNU-IIST, P.O.Box 3058, Macau, June 2006. abstract pdf

 [336]
Xiangpeng Zhao, Antonio Cerone, and Padmanabhan Krishnan. Modelling and Resource Allocation Planning of BPEL Workflows under Security Constraints. Technical Report 336, UNU-IIST, P.O.Box 3058, Macau, June 2006. abstract

 [335]
Xin Chen, Jifeng He, and Zhiming Liu. Component Coordination in rCOS. Technical Report 335, UNU-IIST, P.O.Box 3058, Macau, May 2006. abstract pdf

 [334]
Mike Reed, Chris George, and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2005. Administrative Report 334, UNU-IIST, P.O.Box 3058, Macau, January 2006. abstract pdf

 [333]
Luís Barbosa and Zhiming Liu, editors. Preliminary Proceedings of the Second International Workshop on Formal Aspects of Component Software FACS'05, Macao, October 24-25, 2005, number 333 in UNU-IIST Reports, P.O.Box 3058, Macau, October 2005. abstract pdf

 [332]
Miaomiao Zhang and Dang Van Hung. Formal Analysis of Streaming Downloading Protocol for System Upgrading. Technical Report 332, UNU-IIST, P.O.Box 3058, Macau, December 2005. Presented and published in the proceedings of the 4th Workshop on Quantitative Aspects of Programming Languages (QAPL 06), Vienna, Austria - April 1 - 2, 2006, ENTCS, Elsevier, 2006. abstract pdf

 [331]
Juan Ignacio Perna and Chris George. Model checking RAISE specifications. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau, December 2005. abstract pdf

 [330]
He Jifeng, Xiaoshan Li, and Zhiming Liu. Component-Based Software Engineering - the Need to Link Methods and their Theories. Technical Report 330, UNU-IIST, P.O.Box 3058, Macau, August 2005. Presented at and published in the proceedings of ICTAC05, LNCS 3722, Dang Van Hung and Martin Wirsing (eds), Spinger 2005, pp. 70 - 95. abstract pdf

 [329]
Yining Wei, Xiaoshan Li, Zhiming Liu, and He Jifeng. Automatic Transformation from Requirements models to Executable Prototypes. Technical Report 329, UNU-IIST, P.O.Box 3058, Macau, October 2005. abstract pdf

 [328]
He Jifeng and C.A.R. Hoare. Linking Theories of Concurrency. Technical Report 328, UNU-IIST, P.O.Box 3058, Macau, July 2005. Presented at and published in the proceedings of ICTAC05, LNCS 3722, Dang Van Hung and Martin Wirsing (eds), Spinger 2005, pp. 303 - 317. abstract pdf

 [327]
He Jifeng, Zhiming Liu, and Xiaoshan Li. A Theory of Contracts. Technical Report 327, UNU-IIST, P.O.Box 3058, Macau, July 2005. Published in Electronic Notes of Theoretical Computer Science, Volume 160 , pp. 173-195 2006. abstract pdf

 [326]
Dang Van Hung and Zhang Miaomiao. On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties. Technical Report 326, UNU-IIST, P.O.Box 3058, Macau, June 2005. Presented at and published in the proceedings of the Embedded and Real-Time Computing Systems and Applications RTCSA 2007, Daugu, Korea, August 21-24, 2007, IEEE Society Press, 2007, pp. 165-172. abstract pdf

 [325]
Zhiming Liu. Lecture Notes on Programming Concurrent Computer Systems. Technical Report 325, UNU-IIST, P.O.Box 3058, Macau, May 2005. abstract pdf

 [324]
Quan Long, Zongyan Qiu, Zhiming Liu, Lingshuang Shao, and He Jifeng. POST: A Case Study for rCOS Incremental Development. Technical Report 324, UNU-IIST, P.O.Box 3058, Macau, May 2005. Presented at and published in the proceedings of ICTAC05, LNCS 3722, Dang Van Hung and Martin Wirsing (eds), Spinger 2005, pp. 485 - 500. abstract pdf

 [323]
Zhiming Liu and Mathai Joseph. Real-Time and Fault-Tolerant Systems - Specification, Verification, Refinement and Scheduling. Technical Report 323, UNU-IIST, P.O.Box 3058, Macau, May 2005. abstract pdf

 [322]
He Jifeng, Xiaoshan Li, and Zhiming Liu. A Refinement Calculus for Object Systems. Technical Report 322, UNU-IIST, P.O.Box 3058, Macau, May 2005. Published in Theoretical Computer Science (2006), doi:10.1016/j.tcs.2006.07.034. abstract pdf

 [321]
Percy Antonio Pari Salas and Bernhard K. Aichernig. Automatic Test Case Generation for OCL: a Mutation Approach. Technical Report 321, UNU-IIST, P.O.Box 3058, Macau, May 2005. An improved version of this report was presented and published in the proceedings of QSIC 2005, Melbourne, Australia 2005. abstract pdf

 [320]
Weimin Ge and Yuefeng Chao. Implementation of E-learning System for UNU-IIST. Technical Report 320, UNU-IIST, P.O.Box 3058, Macau, April 2005. abstract pdf

 [319]
Quan Long, Zhiming Liu, Xiaoshan Li, and He Jifeng. Consistent Code Generation from UML Models. Technical Report 319, UNU-IIST, P.O.Box 3058, Macau, April 2005. Presented and published in the proceedings of Australian Software Engineering Conference 2005, IEEE Computer Society Press 2005. abstract pdf

 [318]
Quan Long, He Jifeng, and Zhiming Liu. Refactoring and Pattern-directed Refactoring: A Formal Perspective. Technical Report 318, UNU-IIST, P.O.Box 3058, Macau, January 2005. abstract pdf

 [317]
Dang Van Hung and Bui Vu Anh. Model Checking Component Based Systems with Blackbox Testing. Technical Report 317, UNU-IIST, P.O.Box 3058, Macau, October 2004. Presented and published in the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2005), 17-19 August 2005, Hong Kong, IEEE Computer Society, pp. 76-79. abstract pdf

 [316]
Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Algorithms and Tools. Technical Report 316, UNU-IIST, P.O.Box 3058, Macau, September 2004. abstract pdf

 [315]
Saleem Zougbi. Reconciling the Should-be and the Can-be in Undergraduate Curricula: Lessons from Bethlehem University, Palestine. Technical Report 315, UNU-IIST, P.O.Box 3058, Macau, August 2004

 [314]
Chris George and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2004. Administrative Report 314, UNU-IIST, P.O.Box 3058, Macau, September 2004. abstract pdf

 [313]
Carlo Corrales Delgado and Bernhard K. Aichernig. Test Purpose Generation by Specification Mutation in Distributed Systems. Technical Report 313, UNU-IIST, P.O.Box 3058, Macau, September 2004

 [312]
Ri Chol Gun and Antonio Cerone. Postgraduate Information Systems Curriculum for the University of Natural Science in the DPR of Korea. Technical Report 312, UNU-IIST, P.O.Box 3058, Macau, September 2004

 [311]
Ri Myong Bok. Undergraduate Computer Science Curriculum for the DPR of Korea. Compendia Report 311, UNU-IIST, P.O.Box 3058, Macau, September 2004

 [310]
Zhiming Liu, editor. Proceedings of the First International Colloquium on Theoretical Aspects of Computing ICTAC04, Guiyang, China 20 - 24 September 2004, number 310 in UNU-IIST Reports, P.O.Box 3058, Macau, September 2004. abstract pdf

 [309]
Yang Jing, Long Quan, Li Xiaoshan, and Zhiming Liu. A Predicative Semantic Model for Integrating UML Models. Technical Report 309, UNU-IIST, P.O.Box 3058, Macau, September 2004. Presented at and published in the proceedings of the 1st International Colloquium on Theoretical Aspects of Computing (ICTAC), September 20-24, 2004 Guiyang, China. abstract pdf

 [308]
He Jifeng, Zhiming Liu, Li Xiaoshan, and Qin Shengchao. A Relational Model for Object-Oriented Designs. Technical Report 308, UNU-IIST, P.O.Box 3058, Macau, September 2004. Presented at and published in the proceedings of the Second ASIAN Symposium on Programming Languages and Systems (APLAS) 2004

 [307]
Li Xiaoshan, Zhiming Liu, He Jifeng, and Long Quan. Generating a Prototype from UML Model of System Requirements. Technical Report 307, UNU-IIST, P.O.Box 3058, Macau, September 2004. Presented at and published in the proceedings of the International Conference on Distributed Computing and Internet Technologies (ICDCIT) 2004. abstract pdf

 [306]
Pham Hong Thai and Dang Van Hung. Verifying Linear Duration Constraints of Timed Automata. Technical Report 306, UNU-IIST, P.O.Box 3058, Macau, June 2004. Presented at and published in the proceedings of ICTAC'04, Gui Yang, September, 2004, LNCS 3407, Springer 2005, pp. 295-309. abstract pdf

 [305]
Bhim Prasad Upadhyaya and Zhiming Liu. A Formal Model for JavaBeans. Technical Report 305, UNU-IIST, P.O.Box 3058, Macau, September 2004. Based on this report, a paper titled A Design Level Formal Model for JavaBeans was presented at and published in the proceedings of SCI'04 and a paper titled Formal Support for Development of JavaBeans Component Systems was presented at and published in the proceedings of COMPSAC'04. abstract pdf

 [304]
Elizabeth Vidal Duarte and Bernhard K. Aichernig. Towards an Improved Computing Curriculum for San Pablo Catholic University in Peru. Technical Report 304, UNU-IIST, P.O.Box 3058, Macau, June 2004. abstract pdf

 [303]
Kim Pyong Sam and Dang Van Hung. A UTP Approach Semantics for Component-Based Real-Time Systems. Technical Report 303, UNU-IIST, P.O.Box 3058, Macau, June 2004. abstract pdf

 [302]
Kim Yong Chun and Dang Van Hung. Verifying Real-Time Systems Using Untimed Model Checking Tools. Technical Report 302, UNU-IIST, P.O.Box 3058, Macau, June 2004. abstract pdf

 [301]
Yifeng Chen and Zhiming Liu. From Durational Specifications to TLA Designs of Timed Automata. Technical Report 301, UNU-IIST, P.O.Box 3058, Macau, June 2004. Presented at and published in the proceedings of ICFEM04. abstract pdf

 [300]
Satyajit Acharya and Chris George. Specifying a Mobile Computing Application Environment Using RSL. Technical Report 300, UNU-IIST, P.O.Box 3058, Macau, May 2004. Presented at and published in the proceedings of QSIC 2OO5, Melbourne, Australia, September 2005. abstract pdf

 [299]
Sun Meng, Zhang Naixiao, and Bernhard K. Aichernig. The Formal Foundations in RSL for UML Statechart Diagrams. Technical Report 299, UNU-IIST, P.O.Box 3058, Macau, April 2004. abstract pdf

 [298]
Zhiming Liu, He Jifeng, and Li Xiaoshan. Contract-Oriented Component Software Development. Technical Report 298, UNU-IIST, P.O.Box 3058, Macau, April 2004. Presented at and published in the proceedings of IFIP WCC-TCS2004, 24-26 August 2004, Toulouse, Francepp, pp. 349-366. abstract pdf

 [297]
Dang Van Hung. A Technique for Improving Time Performance for Synchronous Parallel Programs. Technical Report 297, UNU-IIST, P.O.Box 3058, Macau, March 2004. Presented at and published in the proceedings of the National Conference Fundamental and Applied Information Technology Research (FAIR'03), Hanoi, October 4-5, 2003. abstract pdf

 [296]
Dang Van Hung. A Formal Model for Component Interfaces for Real-time Systems. Technical Report 296, UNU-IIST, P.O.Box 3058, Macau, March 2004. Presented at and published in the proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical Systems, September 5-6, 2005, Lisbon, Portugal, Tiziana Margaria and Mieke Massink (eds.), ACM Sigsoft, pp. 106-114. abstract pdf

 [295]
Zhiming Liu, Xiaoshan Li, Jing Liu, and He Jifeng. Integrating and Refining UML Models. Technical Report 295, UNU-IIST, P.O.Box 3058, Macau, March 2004. Presented at the UML2004 Workshop on Consistency Problems in UML-based Software Development, October 10-15, 2004, Lisbon, Portugal, published in Journal on Software and Systems Modeling. abstract pdf

 [294]
Pu Geguang, Jin Naiyong, He Jifeng, and Qiu Zongyan. Performance Analysis in High-Level Synthesis. Technical Report 294, UNU-IIST, P.O.Box 3058, Macau, February 2004. abstract pdf

 [293]
Jing Liu, Zhiming Liu, He Jifeng, and Xiaoshan Li. Linking UML Models of Design and Requirement. Technical Report 293, UNU-IIST, P.O.Box 3058, Macau, February 2004. Presented at and published in the proceedings of ASWEC2004, 13-16 April, 2004, Melbourne, Australia. abstract pdf

 [292]
Xiaoshan Li, Zhiming Liu, and Jifeng He. A Formal Semantics of UML Sequence Diagram. Technical Report 292, UNU-IIST, P.O.Box 3058, Macau, February 2004. Presented at and published in the proceedings of ASWEC2004, 13-16 April, 2004, Melbourne, Australia. abstract pdf

 [291]
Yifeng Chen and Zhiming Liu. Integrating Temporal Logics. Technical Report 291, UNU-IIST, P.O.Box 3058, Macau, February 2004. Presented at and published in the proceedings of IFM 2004, 4-7 April, 2004, Canterbury, Kent, UK, Eerke A. Boiten, John Derrick, Graeme Smith (Eds.), LNCS 2999, Springer-Verlag, 2004, pp. 402-420. abstract pdf

 [290]
Chris George and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2003. Administrative Report 290, UNU-IIST, P.O.Box 3058, Macau, March 2004 pdf

 [289]
Gabriel Adenawo and Bernhard K. Aichernig. Mutation Testing in the Unifying Theory of Programming. Technical Report 289, UNU-IIST, P.O.Box 3058, Macau, October 2003

 [288]
Zhiming Liu, He Jifeng, Xiaoshan Li, and Jing Liu. Unifying Views of UML. Technical Report 288, UNU-IIST, P.O.Box 3058, Macau, October 2003. Presented at the UML03 Workshop on Composition Verification of UML Models, 20-24 October 2003, San Francisco, California, USA. abstract pdf

 [287]
Zhiming Liu, He Jifeng, Xiaoshan Li, and Yifeng Chen. A Relational Model for Formal Object-Oriented Requirement Analysis in UML. Technical Report 287, UNU-IIST, P.O.Box 3058, Macau, September 2003. Presented at and published in the proceedings of ICFEM2003, 5-7 November 2003, Singapore, LNCS 2885, Springer-Verlag, 2003, pp 641 - 664. abstract pdf

 [286]
Pu Geguang, Wang Yi, Dang Van Hung, and He Jifeng. An Optimal Approach to Hardware/software Partitioning for Synchronous Model. Technical Report 286, UNU-IIST, P.O.Box 3058, Macau, September 2003. Presented at and published in the proceedings of the IFM 2004 Conference, Canterbury, UK, 4-7 April, 2004, Eerke A. Boiten, John Derrick, Graeme Smith (Eds.), LNCS 2999, Springer-Verlag, 2004, pp. 363-381. An improved version of this paper is accepted by the international journal Formal Aspects of Computing, 2005. abstract pdf

 [285]
He Jifeng, Liu Zhiming, and Li Xiaoshan. Component Calculus. Technical Report 285, UNU-IIST, P.O.Box 3058, Macau, September 2003. Presented as an Invited Talk at Workshop on Formal Aspects of Component Software FACS'03, Satellite Workshop of the FM 2003, Pisa, Italy - September 8-9, 2003. abstract pdf

 [284]
Hung Dang Van and Zhiming Liu, editors. Proceedings of the Workshop on Formal Aspects of Component Software FACS'03, Satellite Workshop of the FM 2003, Pisa, Italy - September 8-9, 2003, number 284 in UNU-IIST Reports, P.O.Box 3058, Macau, September 2003. abstract pdf

 [283]
Pei Yu and Xu Qiwen. Checking Interval Based Properties for Reactive Systems. Technical Report 283, UNU-IIST, P.O.Box 3058, Macau, September 2003. Presented at and published in the proceedings of Fifth International Conference on Verification, Model Checking and Abstract Interpretation, Venice, Italy, LNCS 2937, January 2004. abstract pdf

 [282]
He Jifeng and Tony Hoare. Equating Bisimulation with Refinement. Technical Report 282, UNU-IIST, P.O.Box 3058, Macau, August 2003. abstract pdf

 [281]
Sun Meng and Luis S. Barbosa. On Refinement of Generic Software Components . Technical Report 281, UNU-IIST, P.O.Box 3058, Macau, July 2003. abstract pdf

 [280]
He Jifeng, Liu Zhiming, and Li Xiaoshan. Modelling Object-oriented Programming with Reference Type and Dynamic Binding. Technical Report 280, UNU-IIST, P.O.Box 3058, Macau, May 2003. abstract pdf

 [279]
Abdugani Abdukhamidov and Chris George. Extending the RSL C++ translator to generate SQL. Technical Report 279, UNU-IIST, P.O.Box 3058, Macau, May 2003. abstract

 [278]
He Jifeng. An Operational Approach to Communicating Processes. Technical Report 278, UNU-IIST, P.O.Box 3058, Macau, May 2003. abstract pdf

 [277]
Jin Naiyong and He Jifeng. Resource Semantic Models for Programming Languages. Technical Report 277, UNU-IIST, P.O.Box 3058, Macau, April 2003. abstract pdf

 [276]
He Jifeng, Zhiming Liu, and Li Xiaoshan. Contract-Oriented Component Software Development. Technical Report 276, UNU-IIST, P.O.Box 3058, Macau, April 2003. abstract pdf

 [275]
Ri Hyon Sul and He Jifeng. A Complete Verification System for Timed RSL. Technical Report 275, UNU-IIST, P.O.Box 3058, Macau, March 2003. abstract pdf

 [274]
Choe Sun Yong and Zhiming Liu. Apply Object-Orientation and UML to the Development of Web-based Learning System. Technical Report 274, UNU-IIST, P.O.Box 3058, Macau, March 2003. abstract pdf

 [273]
Li Dan and Bernhard K. Aichernig. Automatic Test Case Generation for RAISE. Technical Report 273, UNU-IIST, P.O.Box 3058, Macau, January 2003. abstract pdf

 [272]
Sun Meng and Bernhard K. Aichernig. Towards a Coalgebraic Semantics of UML: Class Diagrams and Use Cases. Technical Report 272, UNU-IIST, P.O.Box 3058, Macau, January 2003. abstract pdf

 [271]
Sun Meng and Bernhard K. Aichernig. CoalgKPF: Towards a Coalgebraic Calculus for Component-Based Systems. Technical Report 271, UNU-IIST, P.O.Box 3058, Macau, January 2003. abstract pdf

 [270]
Adnan Sherif and He Jifeng. A Framework For The Specification, Verification and Development of Real Time Systems using Circus. Technical Report 270, UNU-IIST, P.O. Box 3058, Macau, November 2002. abstract pdf

 [269]
Dimitar P. Guelev and Dang Van Hung. Projection onto State in Duration Calculus: Relative Completeness. Technical Report 269, UNU-IIST, P.O.Box 3058, Macau, November 2002. Presented at the Third Workshop on Automated Verification of Critical Systems (AVoCS 2003) April 2-3 2003, Southampton (UK), pp. 64-73. An improved version of this paper with the title 'A Relatively Complete Axiomatisation of Projection onto State in the Duration Calculus' is published in the special issue on ITL and DC, Jounal of Applied and Non-Classical Logics, Vol 14, No 1-2, Lavoisier, Paris, 2004, pp. 151-182. abstract pdf

 [268]
Fikayo Ajayi and Dang Van Hung. Translating Duration Calculus Designs into OCCAM Programs. Technical Report 268, UNU-IIST, P.O.Box 3058, Macau, October 2002. abstract pdf

 [267]
Sun Meng and Bernhard K. Aichernig. Component-Based Coalgebraic Specification and Verification in RSL. Technical Report 267, UNU-IIST, P.O.Box 3058, Macau, October 2002. Presented and published in the proceedings of PDCAT 2005, Dalian, China, 2005. abstract pdf

 [266]
Chris George and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2002. Administrative Report 266, UNU-IIST, P.O.Box 3058, Macau, April 2003 pdf

 [265]
Dang Van Hung and Dimitar P. Guelev. Real-Time Systems Refinement with State Projections. Technical Report 265, UNU-IIST, P.O.Box 3058, Macau, October 2002. abstract pdf

 [264]
Yifeng Chen and Zhiming Liu. Linking Temporal Logics. Technical Report 264, UNU-IIST, P.O. Box 3058, Macau, October 2002

 [263]
Zhiming Liu, Xiaoshan Li, and Jifeng He. Using Transition Systems to Unify UML Requirement Models. Technical Report 263, UNU-IIST, P.O. Box 3058, Macau, October 2002. Presented at and published in the proceedings of the 4th International Conference on Formal Engineering Methods (ICFEM 2002), October 22-25, 2002, Shanghai, China, LNCS 2495, Springer-Verlag, 2002, pp 535-547. abstract pdf

 [262]
Jifeng He, Zhiming Liu, and Xiaoshan Li. A Relational Model for Specification of Object-Oriented Systems. Technical Report 262, UNU-IIST, P.O. Box 3058, Macau, October 2002. abstract pdf

 [261]
Arifa Bhutto, Uzma Khadim, and Tomasz Janowski. Developing an XML-Enabled Serials Management System using RAISE. Technical Report 261, UNU-IIST, P.O. Box 3058, Macau, September 2002. abstract pdf

 [260]
Ho Van Huong and Dang Van Hung. Modelling Real-time Database Systems in Duration Calculus. Technical Report 260, UNU-IIST, P.O. Box 3058, Macau, September 2002. Presented at and published in the proceedings of the IASTED International Conference on Databases and Applications (DBA 2004), February 17 - 19, 2004, Innsbruck, Austria, M.H. Hamza (ed.), ACTA Press, pp. 37-42. abstract pdf

 [259]
Zhiming Liu. Software Development with UML. Technical Report 259, UNU-IIST, P.O. Box 3058, Macau, July 2002. abstract pdf

 [258]
Zhiming Liu, Xiaoshan Li, Jifeng He, and Yifeng Chen. A Relational Model for Object-Oriented Requirement Analysis. Technical Report 258, UNU-IIST, P.O. Box 3058, Macau, July 2002. abstract pdf

 [257]
Adnan Sherif and He Jifeng. Towards a Time Model for Circus. Technical Report 257, UNU-IIST, P.O. Box 3058, Macau, July 2002. Presented at and published in the proceedings of the 4th International Conference on Formal Engineering Methods (ICFEM 2002), October 22-25, 2002 Shanghai, China, LNCS 2495, Springer-Verlag, 2002. abstract pdf

 [256]
Aristides Dasso and Chris George. Transforming RSL into PVS. Technical Report 256, UNU-IIST, P.O. Box 3058, Macau, May 2002. abstract pdf

 [255]
Dang Van Hung. Real-time Systems Development with Duration Calculus: an Overview. Technical Report 255, UNU-IIST, P.O. Box 3058, Macau, June 2002. Published in the proceedings for the UNU-IIST 10th Anniversary Colloquium on Formal Methods at the Crossroads, from Panacea to Foundational Support, LNCS 2757, Springer-Verlag, November 2003, pp. 81-96. abstract pdf

 [254]
Bernhard K. Aichernig. The Commuting V-Diagram: On the Relation of Refinement and Testing. Technical Report 254, UNU-IIST, P.O. Box 3058, Macau, May 2002. abstract pdf

 [253]
Ana Funes and Chris George. Formal Foundations in RSL for UML Class Diagrams. Technical Report 253, UNU-IIST, P.O. Box 3058, Macau, May 2002. Published as chapter VIII Formalizing UML Class Diagrams of UML and the Unified Process, Liliana Favre (ed.), IRM Press, 2003. abstract pdf

 [252]
Gafurov Davrondjon and Tomasz Janowski. Developing a Spell-Checker for Tajik using RAISE. Research Report 252, UNU-IIST, P.O. Box 3058, Macau, May 2002. Presented at and published in the proceedings of the ICFEM2002, Shanghai, October 2002, LNCS 2495, Springer-Verlag, 2002. abstract pdf

 [251]
Jifeng He, Zhiming Liu, and Xiaoshan Li. Towards a Refinement Calculus for Object Systems. Research Report 251, UNU-IIST, P.O. Box 3058, Macau, May 2002. Presented at and published in the proceedings of the conference ICCI2002, Canada, July 2002, IEEE Computer Society Press, pp. 69-77. abstract pdf

 [250]
Bernhard K. Aichernig. Contract-based Mutation Testing in the Refinement Calculus. Technical Report 250, UNU-IIST, P.O. Box 3058, Macau, April 2002. Presented at and published in the proceedings of the Refinement Workshop REFINE'02, Copenhagen, Denmark, July 20-21, 2002 (affiliated with FME 2002). abstract pdf

 [249]
Chris George. Introduction to RAISE. Technical Report 249, UNU-IIST, P.O. Box 3058, Macau, April 2002. abstract pdf

 [248]
He Jifeng and Viktor Verbovskiy. Integrating CSP and DC. Technical Report 248, UNU-IIST, P.O. Box 3058, Macau, January 2002. Presented at and published in the proceedings of the 8th IEEE International Conference on Engineering of Complex Computer Systems, Maryland, USA, 2-4 December 2002

 [247]
Li Yong and Dang Van Hung. Checking Temporal Duration Properties of Timed Automata. Technical Report 247, UNU-IIST, P.O. Box 3058, Macau, November 2001. Published in Journal of Computer Science and Technology, Vol. 17, No. 6, November 2002, pp. 689-698. abstract pdf

 [246]
Zhou Chaochen and Wendy Hoi Iok Wa. UNU-IIST Annual Report 2001. Administrative Report 246, UNU-IIST, P.O.Box 3058, Macau, October 2001 pdf

 [245]
Kim Pyong Sam and He Jifeng. Towards a Dynamic Semantics of an Assembly Language. Technical Report 245, UNU-IIST, P.O. Box 3058, Macau, October 2001. abstract

 [244]
Chen Chang and He Jifeng. Hardware/Software Interface Design. Technical Report 244, UNU-IIST, P.O. Box 3058, Macau, October 2001. abstract pdf

 [243]
Xu Qiwen and Zhan Naijun. Formalising Scheduling Theories in Duration Calculus. Technical Report 243, UNU-IIST, P.O. Box 3058, Macau, October 2001. abstract pdf

 [242]
Kim Yong Chun and Dang Van Hung. Specification and Verification of Spatial Data Types with B-Toolkit. Technical Report 242, UNU-IIST, P.O. Box 3058, Macau, October 2001. Presented at and published in the proceedings of the IEEE conference COMPSAC 2002, Oxford, England, August 26-29, 2002, IEEE Computer Society Press, pp. 711-716. abstract pdf

 [241]
Siba K. Udgata and Dang Van Hung. A Formal Model for Channel Allocation in Distributed Mobile Computing Systems. Technical Report 241, UNU-IIST, P.O. Box 3058, Macau, October 2001. A part of the work was presented at and published under the title Distributed Dynamic Channel Assignment in Mobile Cellular Network as a Special Mutual Exclusion Concept in the proceedings of the 4th International Conference on Information Technology (CIT'01), Gopalpur-on-sea, Orissa, India, December 20-22, 2001, A K Pujari and P. K. Mahapatra (Eds.), pp. 23-31, Tata-McGraw Hill Publications, 2001. A revised version of this report was presented at and published in the proceedings of the 2003 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'03) under the title A formal model for dynamic channel allocation as a mutual exclusion concept in a distributed mobile computing system, June 23-26, 2003, Las Vegas, Nevada, USA, Hamid Arabania and Youngsong Mun (eds), CSREA Press, pp. 1464-1468. abstract pdf

 [240]
Adegboyega Ojo and Tomasz Janowski. Formalising Distributed Business Processes. Technical Report 240, UNU-IIST, P.O. Box 3058, Macau, August 2001. Presented at and published in the proceedings of the 2nd International Workshop on Conceptual Modeling Approaches for e-Business (ECOMO2001), Yokohama, Japan, November 2001, Springer Verlag. abstract pdf

 [239]
Lutbat Yadamsuren and Zhiming Liu. A DC-Based Approach to Refinement of Real-time Systems. Technical Report 239, UNU-IIST, P.O.Box 3058, Macau, August 2001. abstract pdf

 [238]
Wang Jinsong, Wang Zheming, and Chris George. A Formal Specification of a Sharable Distance Education Course System. Technical Report 238, UNU-IIST, P.O.Box 3058, Macau, August 2001. abstract pdf

 [237]
Juliano Iyoda and He Jifeng. A Prolog Prototype for the Synthesis of Verilog. Technical Report 237, UNU-IIST, P.O.Box 3058, Macau, July 2001. abstract pdf

 [236]
Dimitar P. Guelev and Dang Van Hung. Prefix and Projection onto State in Duration Calculus. Technical Report 236, UNU-IIST, P.O.Box 3058, Macau, July 2001. Presented at the Workshop on Theory and Practice of Timed Systems, April 6-7, 2002, Grenoble, France. Published in the Electronic Notes in Theoretical Computer Science, Volume 65, Issue 6, Elsevier Science 2002, (http://www.elsevier.com). abstract pdf

 [235]
Xiaoshan Li, Zhiming Liu, and Zhengshen Guo. A Formal Design of Online Ticketing System in UML. Research Report 235, UNU-IIST, P.O. Box 3058, Macau, July 2001. Presented at and published in the proceedings of the Asian Pacific Software Engineering Conference, APSEC 2001, IEEE Society Press, 2001, pp. 259-266. abstract pdf

 [234]
Irshad Kamal Khan. Computer Science Curriculum for Bangladesh. Technical Report 234, UNU-IIST, P.O. Box 3058, Macau, July 2001. abstract pdf

 [233]
Raoudha Beltaifa and Richard Moore. A Software Reuse Infrastructure for an Efficient Reuse Practice. Research Report 233, UNU-IIST, P.O. Box 3058, Macau, May 2001. abstract pdf

 [232]
Wang Yanjie, Wang Zhuo, and Chris George. Supporting Collaborative Design. Research Report 232, UNU-IIST, P.O. Box 3058, Macau, May 2001. Accepted for presentation at and publication in the proceedings of the Fifth International Conference Formal Methods for Open Object-Based Distributed Systems (FMOODS), March 2002, University of Twente, the Netherlands. abstract pdf

 [231]
He Jifeng, Liu Zhiming, and Li Xiaoshan. A Relational Model for Object-Oriented Programming. Research Report 231, UNU-IIST, P.O. Box 3058, Macau, May 2001. abstract pdf

 [230]
Xiaoshan Li, Zhiming Liu, and Jifeng He. Formal and use-case driven requirement analysis in UML. Research Report 230, UNU-IIST, P.O. Box 3058, Macau, March 2001. Presented at and published in the proceedings of COMPSAC'2001, Chicago, USA, IEEE Computer Society Press, 2001, pp. 215-224. abstract pdf

 [229]
Zhiming Liu. Object-Oriented Software Development Using UML. Research Report 229, UNU-IIST, P.O. Box 3058, Macau, March 2001. abstract pdf

 [228]
Zhiming Liu, Jifeng He, and Xiaoshan Li. Formalizing the use of UML in requirement analysis. Research Report 228, UNU-IIST, P.O. Box 3058, Macau, March 2001. Presented at and published in the proceedings of the 2001 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'2001), Las Vegas, USA, (2001). abstract pdf

 [227]
Chris George. RAISE Tools User Guide. Technical Report 227, UNU-IIST, P.O. Box 3058, Macau, February 2001. The tools are available from http://www.iist.unu.edu. abstract pdf

 [226]
Murray L Singer and Zhou Chaochen. UNU-IIST Annual Report 2000. Administrative Report 226, UNU-IIST, P.O.Box 3058, Macau, February 2001. abstract pdf

 [225]
Gabriela Aranda and Richard Moore. Formally Modelling Compound Design Patterns. Technical Report 225, UNU-IIST, P.O. Box 3058, Macau, December 2000. abstract pdf

 [224]
Gabriela Aranda and Richard Moore. GoF Creational Patterns: A Formal Specification. Technical Report 224, UNU-IIST, P.O. Box 3058, Macau, December 2000. abstract pdf

 [223]
Maria Virginia Mauco and Chris George. Using Requirements Engineering to Derive a Formal Specification. Technical Report 223, UNU-IIST, P.O. Box 3058, Macau, December 2000. Based on the report, three conference papers authored by Virginia Mauco, Chris George, and Daniel Riesco have been accepted for presentation: (1) `Deriving the Types of a Formal Specification from a Client-Oriented Technique', 2nd International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, Japan, July 2001, (2) `Heuristics to Structure a Formal Specification in RSL from a Client-Oriented Technique', 1st Annual International Conference on Computer and Information Science (ICIS'01), Orlando, Florida, U.S.A., October 2001, (3) `Using a Scenario Model to Derive the Functions of a Formal Specification', APSEC'2001, Macau, December 2001. abstract pdf

 [222]
François Siewe and Dang Van Hung. Deriving Real-Time Programs from Duration Calculus Specifications. Technical Report 222, UNU-IIST, P.O. Box 3058, Macau, December 2000. Published in the proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2001), Livingston-Edinburgh, Scotland, 4-7 September 2001, LNSC 2144, Springer-Verlag, 2001, pp. 92-97. abstract pdf

 [221]
Hong Ki Thae and Dang Van Hung. Formal Design of Hybrid Control Systems: Duration Calculus Approach. Technical Report 221, UNU-IIST, P.O. Box 3058, Macau, November 2000. Presented at and published in the proceedings of The Twenty-Fiftth Annual International Computer Software and Applications Conference (COMPSAC 2001), October 8-12, 2001, Chicago, USA, IEEE Computer Society Press, 2001, pp. 423-428. abstract pdf

 [220]
Univan Ahn and Chris George. C++ Translator for RAISE Specification Language. Technical Report 220, UNU-IIST, P.O. Box 3058, Macau, November 2000. abstract pdf

 [219]
Nitesh Shrestha and Tomasz Janowski. Model-Based Travel Planning. Technical Report 219, UNU-IIST, P.O. Box 3058, Macau, November 2000. abstract pdf

 [218]
Juliano Iyoda and He Jifeng. Towards an Algebraic Synthesis of Verilog. Technical Report 218, UNU-IIST, P.O. Box 3058, Macau, April 2001. Presented at and published in the proceedings of the 2001 International Conference on Engineering of Reconfigurable systems and algorithms (ERSA'2001), Las Vegas, USA, (2001). abstract pdf

 [217]
Li Yongjian and He Jifeng. Towards Unifying Theories of Verilog - Operational Semantics, Bisimulation and Observation Equivalence. Technical Report 217, UNU-IIST, P.O. Box 3058, Macau, November 2000. Presented at and published in the proceedings of the International Conference on Applied Informatics (AI 2001), Innsbruck, Austria, 2001. abstract pdf

 [216]
Yumbayar Namsrai. Undergraduate Software Engineering Curriculum for Developing Countries. Technical Report 216, UNU-IIST, P.O. Box 3058, Macau, November 2000. abstract pdf

 [215]
Tomasz Janowski. Algorithmics, Introduction to the Science of Computing. Technical Report 215, UNU-IIST, P.O. Box 3058, Macau, October 2000. abstract

 [214]
Li Yong and Dang Van Hung. Checking History Properties of Real-Time Systems. Technical Report 214, UNU-IIST, P.O. Box 3058, Macau, October 2000. abstract pdf

 [213]
Tomasz Janowski and Phan Cong Vinh. Protocol-Based Cooperation in a Virtual Manufacturing Organization. Technical Report 213, UNU-IIST, P.O. Box 3058, Macau, October 2000. Presented at and published in the proceedings of the 2nd IFIP/MASSYVE Working Conference on Infrastructures for Virtual Enterprises, Florianopolis, Brazil, December 2000, Kluwer. abstract pdf

 [212]
Ngolah Cyprian and Chris George. Formal Specification of a Query Expression Generator. Technical Report 212, UNU-IIST, P.O. Box 3058, Macau, September 2000. abstract pdf

 [211]
Manas Ranjan Patra and Richard Moore. A Formal Model of an Agent-mediated Electronic Market. Technical Report 211, UNU-IIST, P.O. Box 3058, Macau, August 2000. Presented at and published in the proceedings of the DIISM 2000 conference in Melbourne, Australia, 15-17 November 2000. abstract pdf

 [210]
Hoang Thi Tung Lam and Chris George. Translation for a Subset of RSL into Java. Technical Report 210, UNU-IIST, P.O. Box 3058, Macau, August 2000. abstract pdf

 [209]
R. K. Ghosh and Chris George. Formal Specification of a Zonal Routing Protocol in Mobile Ad Hoc Network. Technical Report 209, UNU-IIST, P.O. Box 3058, Macau, August 2000. abstract pdf

 [208]
Ke Wei and Chris George. An RSL to SML Translator. Technical Report 208, UNU-IIST, P.O. Box 3058, Macau, August 2000. abstract pdf

 [207]
Andres Flores and Richard Moore. GoF Structural Patterns: A Formal Specification. Technical Report 207, UNU-IIST, P.O. Box 3058, Macau, August 2000. Presented at and published in the proceedings of the IASTED International Conference on Applied Informatics (AI 2001), Innsbruck, Austria, 19-22 February 2001, pp. 625-630. abstract pdf

 [206]
Qin Shengchao and He Jifeng. An Algebraic Approach to Hardware/software Partitioning. Technical Report 206, UNU-IIST, P.O. Box 3058, Macau, June 2000. Presented at and published in the proceedings of the 7th IEEE International Conference on Electronics, Circuits & Systems, Kaslik, Lebanon, 17-20 December 2000. abstract pdf

 [205]
Balkhis Abu Bakar and Tomasz Janowski. Automated Result Verification with AWK. Technical Report 205, UNU-IIST, P.O. Box 3058, Macau, June 2000. Presented at and published in the proceedings of the 6th IEEE International Conference on Engineering of Complex Computer Systems, Tokyo, Japan, September 2000, IEEE Computer Society Press. abstract pdf

 [204]
He Jifeng and Xu Qiwen. An Operational Semantics of a Simulator Algorithm. Technical Report 204, UNU-IIST, P.O.Box 3058, Macau, June 2000. Presented at and published in the proceedings of the 2000 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'2000), Las Vegas, Nevada, USA, June 26-29, 2000. abstract pdf

 [203]
Dimitar P. Guelev. Interpolation and related results on the P-fragment of DC with Iteration. Technical Report 203, UNU-IIST, P.O.Box 3058, Macau, June 2000. abstract pdf

 [202]
Dimitar P. Guelev. A Complete Proof System for First Order Interval Temporal Logic with Projection. Technical Report 202, UNU-IIST, P.O.Box 3058, Macau, June 2000. A revised version of this report was published in the Journal of Logic and Computation, Volume 14, Issue 2, April 2004, pp. 215-249 by Oxford University Press. abstract pdf

 [201]
Luis Reynoso and Richard Moore. GoF Behavioural Patterns: A Formal Specification. Technical Report 201, UNU-IIST, P.O. Box 3058, Macau, May 2000. Presented at and published in the proceedings of the ACIS 2nd International Conference on Software Engineering, Artificial Intelligence, Networking & Parallel/Distributed Computing (SNPD'01), Nagoya, Japan, August 2001, pp. 262-270. abstract pdf

 [200]
Andres Flores, Luis Reynoso, and Richard Moore. A Formal Model of Object-Oriented Design and GoF Design Patterns. Technical Report 200, UNU-IIST, P.O. Box 3058, Macau, July 2000. Presented at and published in the proceedings of FME 2001, Berlin, Germany, 12-16 March 2001, LNCS 2021, Springer Verlag 2001, pp. 223-241. abstract pdf

 [199]
Wang Jianzhong, Xu Qiwen, and Ma Huadong. Modelling and Verification of Network Player System with DCValid. Technical Report 199, UNU-IIST, P.O.Box 3058, Macau, June 2000. Published in the Proceedings of the First Asia-Pacific Conference on Quality Software, Hong Kong, October 2000, IEEE Computer Society Press, pp. 44-49. abstract pdf

 [198]
He Jifeng. An Integrated Approach to Hardware/Software Co-design. Technical Report 198, UNU-IIST, P.O.Box 3058, Macau, June 2000. Presented at and published in the proceedings of the International Conference on Software: Theory and Practice (ICS2000), Yulin Feng, David Notkin and Marie-Claude Gaudel (eds), Beijing, August 21-24, 2000

 [197]
Do Van Nhon and Dang Van Hung. A Systematic Design of Real-time Systems Using Duration Calculus. Technical Report 197, UNU-IIST, P.O.Box 3058, Macau, May 2000. Presented at and published in the proceedings of the 5th World Multiconference on Systemics, Cybernetics and Informatics (SCI 2001), Orlando, USA, July 22-25, 2001, IEEE Computer Society Press, pp. 241-246. abstract pdf

 [196]
Dimitar P. Guelev. Probabilistic Neighbourhood Logic. Technical Report 196, UNU-IIST, P.O.Box 3058, Macau, April 2000. Presented at and published in the proceedings of the 6th International Symposium, Pune, India, September 2000 (FTRTFT'00), LNCS 1926, pp. 264-275. abstract pdf

 [195]
Dimitar P. Guelev. A Complete Fragment of Higher-Order Duration μ-Calculus. Technical Report 195, UNU-IIST, P.O.Box 3058, Macau, April 2000. Presented at and published in the proceedings of the 20th conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS20), New Dehli, India, December 2000, LNCS 1974, pp. 264-276. abstract pdf

 [194]
Jin Zhendong and Richard Moore. Specification of Software Systems for Managing Student Accommodation and a Research Laboratory Network. Technical Report 194, UNU-IIST, P.O. Box 3058, Macau, April 2000. abstract pdf

 [193]
Wu Xiaojun and Richard Moore. Specification of a University Personnel Management System. Technical Report 193, UNU-IIST, P.O. Box 3058, Macau, April 2000. abstract pdf

 [192]
Tomasz Janowski. Distributed Production with Specification-Generated Processes. Technical Report 192, UNU-IIST, P.O. Box 3058, Macau, April 2000. Presented at and published in the proceedings of the 4th IEEE/IFIP International Conference on Information Technology for Balanced Automation Systems in Production and Transportation, Berlin, Germany, September 2000, Kluwer. abstract pdf

 [191]
Dangaasuren Garmaa and Dang Van Hung. A Technique for Improvement of Model-checking Linear Duration Invariants. Technical Report 191, UNU-IIST, P.O.Box 3058, Macau, March 2000. abstract pdf

 [190]
He Jifeng, C. C. Morgan, and A.K. McIver. The Weakest Completion Approach to the Probabilistic Semantics. Technical Report 190, UNU-IIST, P.O.Box 3058, Macau, March 2000. abstract pdf

 [189]
He Jifeng. Derive Enriched Semantics by Calculation. Technical Report 189, UNU-IIST, P.O.Box 3058, Macau, March 2000. abstract pdf

 [188]
Li Shuguang, Jiang Qing, and Chris George. Combining Case-based and Model-based Reasoning: A Formal Specification. Technical Report 188, UNU-IIST, P.O.Box 3058, Macau, March 2000. Presented at and published in the prceedings of APSEC 2000, Singapore, December 2000, IEEE Computer Society Press. abstract pdf

 [187]
Murray L Singer and Zhou Chaochen. UNU-IIST Annual Report 1999. Administrative Report 187, UNU-IIST, P.O.Box 3058, Macau, March 2000. abstract pdf

 [186]
Pak Jong Ok, Ri Hyon Sul, and Chris George. A Management System for a University Library. Technical Report 186, UNU-IIST, P.O. Box 3058, Macau, February 2000. abstract pdf

 [185]
Babatunde Opeoluwa Akinkunmi and Tomasz Janowski. Formalising Reuse with Imperfect Components. Technical Report 185, UNU-IIST, P.O. Box 3058, Macau, February 2000. abstract

 [184]
Wasim Uddin Khan and Xu Qiwen. Formalization of Scheduling for Hard Real Time Systems. Research Report 184, UNU-IIST, P.O. Box 3058, Macau, February 2000. abstract pdf

 [183]
Zhu Huibiao and He Jifeng. A DC-based Semantics for Verilog. Technical Report 183, UNU-IIST, P.O. Box 3058, Macau, January 2000. Presented at and published in the proceedings of the International Conference on Software: Theory and Practice (ICS2000), Yulin Feng, David Notkin and Marie-Claude Gaudel (eds), Beijing, August 21-24, 2000, pp. 421-432. abstract pdf

 [182]
François Siewe and Dang Van Hung. From Continuous Specification to Discrete Design. Technical Report 182, UNU-IIST, P.O. Box 3058, Macau, December 1999. Presented at and published in the proceedings of the International Conference on Software: Theory and Practice (ICS2000), Yulin Feng, David Notkin and Marie-Claude Gaudel (eds), Beijing, August 21-24, 2000, pp. 407-414. abstract pdf

 [181]
Tomasz Janowski, Francisco Moreira, and Rui Sousa. Production Modelling as Shell Programming: Concurrency and Delegation. Technical Report 181, UNU-IIST, P.O. Box 3058, Macau, December 1999. Presented at and published in the proceedings of the IFAC Symposium on Manufacturing, Modeling, Management and Control, Rio, Greece, July 2000, Elsevier. abstract pdf

 [180]
Tomasz Janowski, Francisco Moreira, and Rui Sousa. Production Modelling as Shell Programming: Operations and Processes. Technical Report 180, UNU-IIST, P.O. Box 3058, Macau, December 1999. Presented at and published in the proceedings of the 2nd IFAC/IFIP/IEEE Conference on Management and Control of Production and Logistics, Grenoble, France, July 2000, Elsevier. abstract pdf

 [179]
Jules-Raymond Tapamo. Domain Analysis of a System of Assessment of Natural Resource Usage. Technical Report 179, UNU-IIST, P.O. Box 3058, Macau, November 1999. Presented at and published in the proceedings of the Sixth Maghrebian Conference on Computer Science, Fes, Morocco, 1-3 November 2000. abstract pdf

 [178]
Dang Van Hung. Projections: A Technique for Verifying Real-Time Programs in Duration Calculus. Technical Report 178, UNU-IIST, P.O. Box 3058, Macau, November 1999. Published in the proceedings of the Conference on Information Technology and Education, Ho Chi Minh City, Vietnam, January 2000. abstract pdf

 [177]
Shirnen Nyambaa, Ishdorj Tseren-Onolt, and Richard Moore. A Management System for University Teaching. Technical Report 177, UNU-IIST, P.O. Box 3058, Macau, September 1999. Based on this report, a paper `Formal Specification of a Management System for University Teaching' is accepted for SERP02 in the USA. abstract pdf

 [176]
Jonathan Bowen. Animating the Semantics of VERILOG using Prolog. Technical Report 176, UNU-IIST, P.O.Box 3058, Macau, September 1999. abstract pdf

 [175]
Zhan Naijun. Completeness of Higher-Order Duration Calculus. Technical Report 175, UNU-IIST, P.O.Box 3058, Macau, August 1999. Presenred at and published in the proceedings of the European Conference on Computer Science Logics CSL2000, Fischbachan, Munich, Germany, 22-27 August, 2000. abstract pdf

 [174]
Dong Shuzhen, Xu Qiwen, and Zhan Naijun. A Formal Proof of the Rate Monotonic Scheduler. Research Report 174, UNU-IIST, P.O.Box 3058, Macau, August 1999. Presented at and published in the proceedings of The Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), part of the federated 1999 International Computer Congress, December 13 - 15, 1999, Hong Kong, IEEE Computer Society Press, 1999, pp. 500-507. abstract pdf

 [173]
Yumbayar Namsrai. Mathematics for Computer Science. Technical Report 173, UNU-IIST, P.O. Box 3058, Macau, August 1999. abstract pdf

 [172]
He Jifeng. Integrating Variants of DC. Research Report 172, UNU-IIST, P.O.Box 3058, Macau, August 1999. abstract pdf

 [171]
He Jifeng and Xu Qiwen. Advanced Features of DC and Their Applications. Research Report 171, UNU-IIST, P.O.Box 3058, Macau, August 1999. Presented at and published in the proceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, 13-15 September, 1999, published in the international journal Formal Aspects of Computing, 2003, Volume 15, Number 1, pages 84-99. abstract pdf

 [170]
Myatav Erdenechimeg, Richard Moore, and Yumbayar Namsrai. Traditional Mongolian Script in the ISO/IEC 10646 and Unicode Standards. Technical Report 170, UNU-IIST, P.O.Box 3058, Macau, August 1999. Presented by Myatav Erdenechimeg at the 16th International Unicode Conference, Amsterdam, The Netherlands, 27-30 March 2000, and published in the proceedings, Part 1, Section B2, under the title "Encoding and Implementation Issues in Standardising Traditional Mongolian Script". The Unicode Consortium, March 2000. abstract pdf

 [169]
Zhan Naijun. Another Formal Proof for Deadline Driven Scheduler. Technical Report 169, UNU-IIST, P.O.Box 3058, Macau, August 1999. abstract pdf

 [168]
Li Li and He Jifeng. A Denotational Semantics of Timed RSL using Duration Calculus. Technical Report 168, UNU-IIST, P.O.Box 3058, Macau, July 1999. Presented at and published in the proceedings of The Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), part of the federated 1999 International Computer Congress, December 13 - 15, Hong Kong, IEEE Computer Society Press, 1999, pp. 492-503. abstract pdf

 [167]
Zhou Chaochen, Dimitar P. Guelev, and Zhan Naijun. A Higher-Order Duration Calculus. Technical Report 167, UNU-IIST, P.O.Box 3058, Macau, July 1999. Presented at and published in the proceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, 13-15 September, 1999. abstract pdf

 [166]
He Jifeng. A behavioural Model for Co-design. Technical Report 166, UNU-IIST, P.O.Box 3058, Macau, June 1999. Presented at and published in the Proceedings of the World Congress of Formal Methods, Toulouse, France, September, 1999, LNCS 1709, Springer-Verlag, 1999, pp. 1420-1439. abstract pdf

 [165]
Huang Biqing, Tomasz Janowski, and Liu Yonghe. Automating Partner Selection for a Virtual Organisation. Technical Report 165, UNU-IIST, P.O.Box 3058, Macau, May 1999. IFIP/PRODNET Working Conference on Infrastructures for Industrial Virtual Enterprises, Porto, Portugal, October 1999, Kluwer Academic Publishers. abstract pdf

 [164]
Tomasz Janowski and Wojciech Mostowski. Fail-Stop Software Components by Pattern Matching. Technical Report 164, UNU-IIST, P.O.Box 3058, Macau, May 1999. Presented at the Workshop on Run-Time Result Verification, part of the Federated Logic Conference, Trento, Italy, July 1999. Presented at and published at the IFIP 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, Stanford University, USA, September 2000, Kluwer. abstract pdf

 [163]
Dang Van Hung and Dimitar P. Guelev. Completeness and Decidability of a Fragment of Duration Calculus with Iteration. Technical Report 163, UNU-IIST, P.O.Box 3058, Macau, April 1999. Presented at International Conference on Mathematical Foundation of Informatics, Hanoi, October 25-28, 1999. Presented at and published in the proceedings of Asian Computing Science Conference (ASIAN'99), Phuket, Thailand, December 10-12, 1999, P.S. Thiagarajan and R. Yap (eds), Advances in Computing Science, LNCS 1742, Springer-Verlag, 1999, pp. 139-150. A thoroughly revised version of this paper with the title 'On the Completeness and Decidability of Duration Calculus with Iteration' is published in Theoretical Computer Science Journal, Vol 337/1-3 pp 278-304, Elsevier, 2005. abstract pdf

 [162]
Tran Van Dung and He Jifeng. A Theory of Combinational programs. Technical Report 162, UNU-IIST, P.O.Box 3058, Macau, April 1999. Presented at and published in the proceedings of the Asian Pacific Software Engineering Conference, APSEC 2001, IEEE Computer Society Press, 2001, pp. 325-328. abstract pdf

 [161]
Li Li and He Jifeng. Towards a Denotational Semantics of Timed RSL using Duration Calculus. Technical Report 161, UNU-IIST, P.O.Box 3058, Macau, April 1999. Publication by Chinese Journal of Advanced Software Research in 2000. abstract pdf

 [160]
Avirmed Amar, Myatav Erdenechimeg, and Richard Moore. Implementation of the MultiScript Multi-lingual Document Processing System. Technical Report 160, UNU-IIST, P.O.Box 3058, Macau, March 1999. abstract

 [159]
He Bin and Chris George. Formally Describing Intelligent CAD. Technical Report 159, UNU-IIST, P.O.Box 3058, Macau, March 1999. abstract pdf

 [158]
Wang Hanpin and Xu Qiwen. Temporal Logics over Infinite Intervals. Technical Report 158, UNU-IIST, P.O.Box 3058, Macau, March 1999. Published in the journal Discrete Applied Mathematics. abstract pdf

 [157]
Margaret Stuart and Zhou Chaochen. UNU-IIST Annual Report 1998. Administrative Report 157, UNU-IIST, P.O.Box 3058, Macau, February 1999. Richard Moore (editor).

 [156]
Than Quoc Dang and Richard Moore. Formal Modelling of Future Demand Forecasting and Frequent Flyer Programs. Technical Report 156, UNU-IIST, P.O.Box 3058, Macau, February 1999. abstract pdf

 [155]
Hou Jianmin and Dang Van Hung. Verifying Linear Duration Properties of Probabilistic Real-Time Systems. Technical Report 155, UNU-IIST, P.O.Box 3058, Macau, February 1999. abstract pdf

 [154]
Chris George. Proving Safety of Authentication Protocols: a Minimal Approach. Technical Report 154, UNU-IIST, P.O.Box 3058, Macau, February 1999. Presented at and published in the proceedings of the International Conference on Software: Theory and Practice (ICS2000), Yulin Feng, David Notkin and Marie-Claude Gaudel (eds), Beijing, August 21-24, 2000, pp. 492-499. abstract pdf

 [153]
Chris George. A RAISE Tutorial. Technical Report 153, UNU-IIST, P.O.Box 3058, Macau, December 1998. Presented at the BRNS workshop Verification of Digital and Hybrid Systems at TIFR, Mumbai, India, 7-11 January 1999. abstract pdf

 [152]
Ekaterina Pavlova and Dang Van Hung. A Formal Specification of the Concurrency Control in Real-Time Databases. Technical Report 152, UNU-IIST, P.O.Box 3058, Macau, January 1999. Published in the proceedings of 6th Asia-Pacific Software Engineering Conference (APSEC'99) Takamatsu, Japan, December 7-10, 1999, IEEE Computer Society Press, pp. 94-101. abstract pdf

 [151]
Alejandra Cechich and Richard Moore. A Formal Specification of GoF Design Patterns. Technical Report 151, UNU-IIST, P.O.Box 3058, Macau, January 1999. Presented at and published in the proceedings of 6th Asia-Pacific Software Engineering Conference (APSEC'99) Takamatsu, Japan, December 7-10, 1999, IEEE Computer Society Press, pp. 284-291. abstract pdf

 [150]
He Hua. A Prettyprinter for the RAISE Specification Language. Technical Report 150, UNU-IIST, P.O.Box 3058, Macau, December 1998. abstract pdf

 [149]
Chris George and Xia Yong. An Operational Semantics for Timed RAISE. Technical Report 149, UNU-IIST, P.O.Box 3058, Macau, November 1998. Presented at and published in the proceedings of FM'99, Toulouse, France, 20-24 September 1999, LNCS 1709, Springer-Verlag, 1999, pp. 1008-1027. abstract pdf

 [148]
Sheila A. Karipel and Dang Van Hung. A Formal Specification of an Information Processing System in Duration Calculus. Technical Report 148, UNU-IIST, P.O.Box 3058, Macau, October 1998. A revised version of the report was presented at and published in the proceedings of the 4th world multiconference on systematics, cybernetics and informatics (SCI2000), July 23-26, 2000 at Sheraton World Resort, Orlando, Florida, USA, Belkis Sanchez et al (eds), pp 334-339. abstract pdf

 [147]
Gerardo Schneider and Xu Qiwen. Towards an Operational Semantics of Verilog. Technical Report 147, UNU-IIST, P.O.Box 3058, Macau, October 1998. abstract pdf

 [146]
William S. Shu and Richard Moore. Dynamically Reconfigurable University I: Formally Specifying Core Operations. Technical Report 146, UNU-IIST, P.O.Box 3058, Macau, September 1998. abstract pdf

 [145]
Zhao Jianhua and Dang Van Hung. Checking Timed Automata for Some Discretisable Duration Properties. Technical Report 145, UNU-IIST, P.O.Box 3058, Macau, August 1998. Published in "Journal of Computer Science and Technology", Volume 15, Number 5, September 2000, pp. 423-429. abstract pdf

 [144]
Dimitar P. Guelev. Probabilistic Interval Temporal Logic. Technical Report 144, UNU-IIST, P.O.Box 3058, Macau, August 1998. abstract pdf

 [143]
Toshiyuki Tanaka and Chris George. Proving Properties of a Security Protocol Specified in RSL. Technical Report 143, UNU-IIST, P.O.Box 3058, Macau, August 1998. A paper in Japanese based on this work is being published by IPSJ-SIGMPS (Information Processing Society of Japan - SIG in Mathematical modeling and Problem Solving). abstract pdf

 [142]
Hrushikesha Mohanty and Chris George. Specifying a Communication Protocol and Composing Transaction Schedules for a Mobile Environment. Technical Report 142, UNU-IIST, P.O.Box 3058, Macau, August 1998. abstract pdf

 [141]
Dimitar P. Guelev. Iteration of Simple Formulas in Duration Calculus. Technical Report 141, UNU-IIST, P.O.Box 3058, Macau, June 1998. abstract pdf

 [140]
Nilagiri Sathya Prakash, D H S Sarma, and Chris George. Port Management: Domain Analysis. Technical Report 140, UNU-IIST, P.O.Box 3058, Macau, May 1998. abstract pdf

 [139]
Dimitar P. Guelev. A Calculus of Durations on Abstract Domains: Completeness and Extensions. Technical Report 139, UNU-IIST, P.O.Box 3058, Macau, May 1998. abstract pdf

 [138]
Tomasz Janowski and Yun Xiaochun. Concurrency, Faults and Atomic Transactions: Incremental Design for Fault-Tolerance. Technical Report 138, UNU-IIST, P.O.Box 3058, Macau, March 1998. Presented at and published in the proceedings of the Conference on Information Technology and Education, Ho Chi Minh City, Vietnam, January 2000. abstract pdf

 [137]
Tomasz Janowski, Zheng Hongjun, and Gustavo Giménez Lugo. Market-Driven Symbolic Execution of Models of Manufacturing Enterprises. Technical Report 137, UNU-IIST, P.O.Box 3058, Macau, March 1998. 2nd IEEE International Conference on Formal Engineering Methods, Brisbane, Australia, December 1998. IEEE Computer Press. abstract pdf

 [136]
Xu Qiwen and Mohalik Swarup. Compositional Reasoning Using Assumption - Commitment Paradigm. Technical Report 136, UNU-IIST, P.O.Box 3058, Macau, February 1998. Published in International Symposium, Compositionality - The Significant Difference, Hans Langmaack and Amir Pnueli and Willem-Paul de Roever (eds), LNCS 1536, pp. 565-583, Springer-Verlag, 1998. abstract pdf

 [135]
Victor A. Braberman and Dang Van Hung. On Checking Timed Automata for Linear Duration Invariants. Technical Report 135, UNU-IIST, P.O.Box 3058, Macau, February 1998. Presented at and published in the proceedings of the 19th IEEE Real-Time Systems Symposium RTSS'98, December 2-4, 1998, Madrid, Spain, IEEE Computer Society Press, 1998, pp. 264-273. abstract pdf

 [134]
Tran Manh Thang, Nguyen Hong Viet, and Richard Moore. Flight Effectiveness Analysis in Airline Business: A Formal Model. Technical Report 134, UNU-IIST, P.O.Box 3058, Macau, February 1998. abstract pdf

 [133]
Gerardo Schneider and Xu Qiwen. Towards a Formal Semantics of Verilog Using Duration Calculus. Technical Report 133, UNU-IIST, P.O.Box 3058, Macau, February 1998. Presented at and published in the proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, Lyngby, Denmark, September 1998 (FTRTFT'98), Anders P. Ravn and Hans Rischel (Eds.), LNCS 1486, pp. 282-293, Springer-Verlag, 1998. abstract pdf

 [132]
Marcel Fouda and Richard Moore. Formal Modelling of Spatial Information Systems. A Case Study: Water Resources Management. Technical Report 132, UNU-IIST, P.O.Box 3058, Macau, February 1998. abstract pdf

 [131]
Tomasz Janowski, Gustavo Giménez Lugo, and Zheng Hongjun. Composing Enterprise Models: The Extended and The Virtual Enterprise. Technical Report 131, UNU-IIST, P.O.Box 3058, Macau, January 1998. 3rd IEEE/IFIP International Conference Information Technology For Balanced Automation Systems in Manufacturing, Prague, Czech Republic, August 1998, Chapman and Hall. Revised paper Modelling an Extended/Virtual Enterprise by the Composition of Enterprise Models is going to appear in Journal of Intelligent and Robotic Systems, Kluwer. abstract pdf

 [130]
Zhao Jianhua and Dang Van Hung. On Checking Real-Time Parallel Systems for Linear Duration Properties. Technical Report 130, UNU-IIST, P.O.Box 3058, Macau, January 1998. Presented at and published in the proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, Lyngby, Denmark, September 1998 (FTRTFT'98), Anders P. Ravn and Hans Rischel (Eds.), LNCS 1486, pp. 241-250, Springer-Verlag, 1998. A paper based on this report with the title "Automatic Verification of a Class of Concurrent Real-time Systems" has been published in Journal of Software, 2000, 11(2), Beijing, China. abstract pdf

 [129]
Tsend Ganbat and Richard Moore. Specifications of Public Service Systems: Four Case Studies for Use in Lecture Courses on RAISE. Technical Report 129, UNU-IIST, P.O.Box 3058, Macau, January 1998. abstract pdf

 [128]
Gao Jianping and Xu Qiwen. Rigorous Design of a Fault Diagnosis and Isolation Algorithm. Technical Report 128, UNU-IIST, P.O.Box 3058, Macau, December 1997. Presented at and selected for publishing in the proceedings of the Fifth International Workshop on Hybrid Systems, Indiana, USA, 11-13 September, 1997. abstract pdf

 [127]
Bo Stig Hansen and Prashant Gajjar. UNU Financial Administration: Domain Description, Model and Requirements. Technical Report 127, UNU-IIST, P.O.Box 3058, Macau, November 1997. abstract pdf

 [126]
Xia Yong. DC/RJ: A Justification Assistant for Duration Calculus. Technical Report 126, UNU-IIST, P.O.Box 3058, Macau, November 1997. A revised version entitled "A RAISE Specification Framework and Justification Assistant for the Duration Calculus" was presented at and published in the proceedings of ESSLLI-98 Workshop on Duration Calculus, Germany, August, 1998, pp. 51-57. abstract pdf

 [125]
Paritosh K. Pandya, Wang Hanpin, and Xu Qiwen. Towards a Theory of Sequential Hybrid Programs. Technical Report 125, UNU-IIST, P.O.Box 3058, Macau, October 1997. Presented at and published in the proceedings of IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), 8-12 June 1998, Shelter Island, New York, USA, David Gries and Willem-Paul de Roever (eds), Chapman & Hall, 1998, pp. 366-384. abstract pdf

 [124]
Margaret Stuart and Zhou Chaochen. UNU-IIST Annual Report 1997. Administrative Report 124, UNU-IIST, P.O.Box 3058, Macau, October 1997

 [123]
Qiu Zongyan and Zhou Chaochen. A Combination of Interval Logic and Linear Temporal Logic. Technical Report 123, UNU-IIST, P.O.Box 3058, Macau, September 1997. Presented at ComBaS Group, Technical University of Denmark, Copenhagen, Denmark, 4-7 September, 1997. Presented at and published in the proceedings of IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), 8-12 June 1998, Shelter Island, New York, USA, David Gries and Willem-Paul de Roever (eds), Chapman & Hall, 1998, pp. 444-461. abstract pdf

 [122]
Paritosh K. Pandya and Dang Van Hung. Duration Calculus with Weakly Monotonic Time. Technical Report 122, UNU-IIST, P.O.Box 3058, Macau, September 1997. Presented at and published in the proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, Lyngby, Denmark, September 1998 (FTRTFT'98), Anders P. Ravn and Hans Rischel (Eds.), LNCS 1486, pp. 55-64, Springer-Verlag, 1998. abstract pdf

 [121]
Vladimir Zadorozhny. Orthogonal Formalisation of CORBA. Technical Report 121, UNU-IIST, P.O.Box 3058, Macau, August 1997. abstract pdf

 [120]
Rana Barua and Zhou Chaochen. Neighbourhood Logics : NL and NL2. Research Report 120, UNU-IIST, P.O.Box 3058, Macau, August 1997. Presented at ComBaS Group, Technical University of Denmark, Copenhagen, Denmark, 4-7 September, 1997. abstract pdf

 [119]
Tomasz Janowski. Semantics and Logic for Provable Fault-Tolerance, A Tutorial. Research Report 119, UNU-IIST, P.O.Box 3058, Macau, August 1997. Presented at: Formal Methods Europe, September 1997, Graz, Austria; European Conference on Theory and Practice of Software, Lisbon, Portugal, March 1998; and Asian Computing Science Conference, Manila, The Philippines, December 1998, Springer Verlag. abstract pdf

 [118]
Pham Hong Thai and Dang Van Hung. Checking a Regular Class of Duration Calculus Models for Linear Duration Invariants. Technical Report 118, UNU-IIST, P.O.Box 3058, Macau, July 1997. Presented at and published in the Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE'98), 20 - 21 April 1998, Kyoto, Japan, Bernd Kramer, Naoshi Uchihira, Peter Croll and Stefano Russo (Eds), IEEE Computer Society Press, 1998, pp. 61 - 71. abstract pdf

 [117]
Vladimir Zadorozhny. Towards an integrated CORBA/RAISE Semantic Interoperable Environment. Technical Report 117, UNU-IIST, P.O.Box 3058, Macau, July 1997. abstract pdf

 [116]
Arun K Pujari. Neighbourhood Logic & Interval Algebra. Technical Report 116, UNU-IIST, P.O.Box 3058, Macau, July 1997. abstract pdf

 [115]
Do Tien Dung, Chris George, Hoang Xuan Huan, and Phung Phuong Nam. A Financial Information System. Technical Report 115, UNU-IIST, P.O.Box 3058, Macau, July 1997. Partly published in Requirements Targeting Software and Systems Engineering, LNCS 1526, Springer-Verlag, 1998. abstract pdf

 [114]
Aristides Dasso. A Course on Formal Methods Using RAISE. Technical Report 114, UNU-IIST, P.O.Box 3058, Macau, June 1997. A paper An Application of Formal Methods: Specifying a Credit Card System based on this work was presented at the IASTED conference on Software Engineering, October 1998 in Las Vegas, USA. A further paper A Technique to Induce Formal Specifications at The Early Stages of System Development will be presented at the IASTED conference on Software Engineering and Applications, October 6-9, 1999, in Scottsdale, Arizona, USA. abstract pdf

 [113]
Myatav Erdenechimeg and Richard Moore. MultiScript III: Creating and Editing Multi-lingual Documents. Technical Report 113, UNU-IIST, P.O.Box 3058, Macau, September 1997. Revised June 1998. abstract pdf

 [112]
Yumbayar Namsrai and Richard Moore. MultiScript II: Displaying and Printing Multi-lingual Documents. Technical Report 112, UNU-IIST, P.O.Box 3058, Macau, June 1997. A part of the work has been presented at and published in the proceedings of the Workshop on the Principles of Digital Document Processing, March 1998, St. Malo, France, Ethan V. Munson, Charles Nicholas and Derick Wood (Eds), Lecture Notes in Computer Science 1481, Springer Verlag, 1998, pages 70 - 81. abstract

 [111]
Marisa Sanchez. Specification-based Testing. Technical Report 111, UNU-IIST, P.O.Box 3058, Macau, June 1997. abstract pdf

 [110]
Gueorgui Satchok. Metropolitan In-street On-route Passenger Transport: Monitoring and Control. Technical Report 110, UNU-IIST, P.O.Box 3058, Macau, June 1997. abstract pdf

 [109]
Li Xuan Dong, Dang Van Hung, and Zheng Tao. Checking Hybrid Automata for Linear Duration Invariants. Research Report 109, UNU-IIST, P.O.Box 3058, Macau, June 1997. Published in R.K.Shamasundar, K.Ueda (Eds.), Advances in Computing Science, Lecture Notes in Computer Science 1345, Springer-Verlag 1997, pp. 166-180. abstract pdf

 [108]
Souleymane Koussoubé. Knowledge-Based Systems: Formalisation and Applications to Insurance. Research Report 108, UNU-IIST, P.O.Box 3058, Macau, May 1997. abstract pdf

 [107]
Roger Noussi. An Efficient Construction of a Domain Theory for Resources Management: A Case Study. Research Report 107, UNU-IIST, P.O.Box 3058, Macau, May 1997. abstract pdf

 [106]
Hoang Thi Tung Lam and Richard Moore. Specification of a Switching Communications System. Technical Report 106, UNU-IIST, P.O.Box 3058, Macau, May 1997. abstract pdf

 [105]
Myatav Erdenechimeg, Richard Moore, and Yumbayar Namsrai. MultiScript I: The Basic Model of Multi-lingual Documents. Technical Report 105, UNU-IIST, P.O.Box 3058, Macau, June 1997. A part of the work has been presented at and published in the proceedings of the Workshop on the Principles of Digital Document Processing, March 1998, St. Malo, France, Ethan V. Munson, Charles Nicholas and Derick Wood (Eds), Lecture Notes in Computer Science 1481, Springer Verlag, 1998, pages 70 - 81. abstract pdf

 [104]
Jose Nuno Oliveira. SETS -- A Data Structuring Calculus and Its Application to Program Development. Research Report 104, UNU-IIST, P.O.Box 3058, Macau, May 1997. Lecture Notes of SETS Calculus Course, UNU-IIST, 5-16 May 1997.

 [103]
Dang Van Hung. Modelling and Verification of Biphase Mark Protocols in Duration Calculus Using PVS/DC-. Research Report 103, UNU-IIST, P.O.Box 3058, Macau, April 1997. Presented at and published in the Proceedings of the 1998 International Conference on Application of Concurrency to System Design (CSD'98), 23-26 March 1998, Aizu-wakamatsu, Fukushima, Japan, IEEE Computer Society Press, 1998, pp. 88 - 98. abstract pdf

 [102]
Dines Bjørner, Souleymane Koussoubé, and Roger Noussi. Jackson's Problem Frames: Syntax, Semantics and Pragmatics; Domains, Requirements and Design. Research Report 102, UNU-IIST, P.O.Box 3058, Macau, April 1997. abstract pdf

 [101]
Fu Hongguang, Yang Lu, and Zhou Chaochen. A Computer-Aided Geometric Approach to Inverse Kinematics. Research Report 101, UNU-IIST, P.O.Box 3058, Macau, April 1997. Published in Journal of Robotic Systems, Vol.15, No.3, pp. 131-143, March 1998. abstract pdf

 [100]
Jan A. Bergstra, Cornelis A. Middelburg, and B. Warinschi. Timed Frame Model for Discrete Time Process Algebra. Research Report 100, UNU-IIST, P.O.Box 3058, Macau, October 1997. abstract pdf

 [99]
Jan A. Bergstra, Cornelis A. Middelburg, and Y.S. Usenko. Discrete-time Process Algebra and the Semantics of SDL. Research Report 99, UNU-IIST, P.O.Box 3058, Macau, October 1997. Published in Jan A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra, Elsevier, 1999, pp. 1209-1268. abstract pdf

 [98]
Jan A. Bergstra, Cornelis A. Middelburg, and R. Soricut. Discrete Time Network Algebra for a Semantic Foundation of SDL. Research Report 98, UNU-IIST, P.O.Box 3058, Macau, October 1997. abstract pdf

 [97]
Suman Roy and Zhou Chaochen. Notes on Neighborhood Logic. Research Report 97, UNU-IIST, P.O.Box 3058, Macau, February 1997. abstract pdf

 [96]
Dines Bjørner. Models of Financial Services & Industries. Research Report 96, UNU-IIST, P.O.Box 3058, Macau, January 1997. Incomplete Draft Report.

 [95]
Dines Bjørner. LSD: Logical Systems Development. Research Report 95, UNU-IIST, P.O.Box 3058, Macau, January 1997. Draft Compendium. Incomplete. Not for circulation

 [94]
Dines Bjørner et al., editors. Design Calculi in Action -- Five Years of R&D at UNU-IIST, number 94 in UNU-IIST Reports, P.O.Box 3058, Macau, January 1997. Vols. I-V. Approx. 2,000 pages. Draft Compendium. Controlled Circulation.

 [93]
Dines Bjørner, Chris George, Bo Stig Hansen, Hans Laustrup, and Søren Prehn. A Railway System, Coordination'97, Case Study Workshop Example. Research Report 93, UNU-IIST, P.O.Box 3058, Macau, January 1997. This is currently a draft report. abstract pdf

 [92]
Tomasz Janowski, Rumel V. Atienza, and Gustavo Giménez Lugo. Integrating Enterprise Models and Models for Marketing Analysis. Research Report 92, UNU-IIST, P.O.Box 3058, Macau, January 1997, Revised September 1998. 2nd IFIP Conference Design of Information Infrastructure Systems for Manufacturing, Denver, USA, May 1998. Chapman and Hall. abstract pdf

 [91]
Zhou Chaochen and Michael R. Hansen. An Adequate First Order Interval Logic. Research Report 91, UNU-IIST, P.O.Box 3058, Macau, December 1996. Published in International Symposium, Compositionality - The Significant Difference, Hans Langmaack and Amir Pnueli and Willem-Paul de Roever (eds), Springer-Verlag, 1998. abstract pdf

 [90]
Dines Bjørner. UN's Software Technology R&D in Africa, Asia, Eastern Europe, and Latin America -- A Personal View. Research Report 90, UNU-IIST, P.O.Box 3058, Macau, December 1996. abstract pdf

 [89]
Dines Bjørner et al. LSD: Logical Systems Development. Lecture Note Compendium 89, UNU-IIST, P.O.Box 3058, Macau, Summer 1996. The report has been replaced by UNU-IIST Report 95. abstract

 [88]
Nikolaj Nikitchenko. Towards Foundations of the General Theory of Transport Domains. Research Report 88, UNU-IIST, P.O.Box 3058, Macau, December 1996. abstract pdf

 [87]
Jan A. Bergstra and Cornelis A. Middelburg. Process Algebraic Underpinning of Communication and Timing in SDL. Research Report 87, UNU-IIST, P.O.Box 3058, Macau, December 1996. abstract pdf

 [86]
Manoranjan Satpathy, Dang Van Hung, and Paritosh K. Pandya. Some Results on The Decidability of Duration Calculus under Synchronous Interpretation. Research Report 86, UNU-IIST, P.O.Box 3058, Macau, December 1996. Presented at the 5th Vietnamese Conference of Mathematics, Hanoi, 17-20 Sep, 1997, presented at and published in the proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, Lyngby, Denmark, September 1998 (FTRTFT'98), Anders P. Ravn and Hans Rischel (Eds.), LNCS 1486, pp. 186-197, Springer-Verlag, 1998. abstract pdf

 [85]
Dines Bjørner. UNU-IIST Annual Report 1996. Administrative Report 85, UNU-IIST, P.O.Box 3058, Macau, October 1996. Margaret Stuart (editor).

 [84]
Nguyen Quoc Toan. An Example for the RAISE Development method: University School Administration. Technical Report 84, UNU-IIST, P.O.Box 3058, Macau, September 1996. abstract pdf

 [83]
Tan Xinming. Enquiring about Bus Transport-Formal Deve