Annual Report 2000

Contents

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

[3]
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.

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

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

[6]
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.

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

[8]
Jonathan Bowen and He Jifeng. An approach to the specification and verification of a hardware compilation scheme. Journal of Supercomputing, 2000.

[9]
Jonathan Bowen, He Jifeng, and Xu Qiwen. An animatable operational semantics of the verilog harware description language. In Proceedings of ICFEM'2000, pages 199-207, York, UK, September 2000. IEEE Computer Society Press.

[10]
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.

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

[12]
Myatav Erdenechimeg and Richard Moore. Multi-directional Multi-lingual Script Processing. Technical Report 75, UNU/IIST, P.O.Box 3058, Macau, June 1996. Published in Proceedings of the Seventeenth International Conference on the Computer Processing of Oriental Languages, Hong Kong, April 2 - 4, 1997, under the title Multi-directional Multilingual Script Processing.

[13]
Myatav Erdenechimeg and Richard Moore. MultiScript III: Creating and Editing Multilingual Documents. Technical Report 113, UNU/IIST, P.O.Box 3058, Macau, September 1997. Revised June 1998.

[14]
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.

[15]
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.

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

[17]
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. To be presented at and published in the proceedings of FME 2001, Berlin, Germany, 12-16 March 2001.

[18]
Dangaasuren Garmaa and Dang Van Hung. A Technique for Improvement of Modelchecking Linear Duration Invariants. Technical Report 191, UNU/IIST, P.O.Box 3058, Macau, March 2000.

[19]
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.

[20]
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.

[21]
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.

[22]
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.

[23]
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.

[24]
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.

[25]
Ma Huadong, Xu Qiwen, and He Jifeng. Formal specification of multimedia synchronisation protocal in dc. In Proceedings of the EEE Pacific Rim Conference on Multimedia 2000, pages 124-129, Australia, 2000.

[26]
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.

[27]
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.

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

[29]
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.

[30]
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.

[31]
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.

[32]
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 and published at the IFIP 4th International Conference on Formal Methods for Open Object-Based Distributed Systems, Stanford University, USA, September 2000, Kluwer.

[33]
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.

[34]
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.

[35]
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.

[36]
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.

[37]
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.

[38]
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.

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

[40]
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.

[41]
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.

[42]
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.

[43]
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.

[44]
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.

[45]
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.

[46]
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.

[47]
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.

[48]
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.

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

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

[51]
Yumbayar Namsrai and Richard Moore. MultiScript II: Displaying and Printing Multilingual 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.

[52]
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.

[53]
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.

[54]
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.

[55]
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.

[56]
Luis Reynoso and Richard Moore. GoF Behavioural Patterns: A Formal Specification. Technical Report 201, UNU/IIST, P.O. Box 3058, Macau, May 2000.

[57]
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.

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

[59]
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.

[60]
Fran,cois 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.

[61]
Fran,cois 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.

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

[63]
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.

[64]
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.

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

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

[67]
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.

[68]
Ly Yongjian and He Jifeng. Towards Unifying Theories of Verilog - Part 1: Operational Semantics, Bisimulation and Observation Equivalence. Technical Report 217, UNU/IIST, P.O. Box 3058, Macau, November 2000.

[69]
Ly Yongjian and He Jifeng. Towards Unifying Theories of Verilog - Part 2: The Algebraic Laws of Verilog. Technical Report 218, UNU/IIST, P.O. Box 3058, Macau, November 2000.

[70]
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.

Annual Report 2000

Contents