Annual Report 1999

Contents

References

 [1]

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

 [2]

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.

 [3]

Rana Barua and Zhou Chaochen. Neighbourhood Logics : NL and NL². 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.

 [4]

J.A. Bergstra, C.A. Middelburg, and Y.S. Ussenko. Discrete-time Process Algebra and the Semantics of SDL. Research Report 99, UNU/IIST, P.O.Box 3058, Macau, October 1997. To appear in J.A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra, Elsevier, 1999.

 [5]

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

 [6]

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.

 [7]

Dines Bjørner, Chris George, and Søren Prehn. Scheduling and Rescheduling of Trains. Research Report 52, UNU/IIST, P.O.Box 3058, Macau, December 1995. Published in Industrial-Strength Formal Methods in Practice, Mike Hinchey and Jonathan Bowen (eds), Springer-Verlag, September 1999.

 [8]

Jonathan Bowen. Animating the Semantics of VERILOG using Prolog. Technical Report 176, UNU/IIST, P.O.Box 3058, Macau, September 1999.

 [9]

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.

 [10]

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.

 [11]

Hu Chenjun, Wang Ji, and Chen Huowang. A labelled sequent calculus for the interval temporal logic. Journal of Computer, China, 1999.

 [12]

Hu Chenjun, Wang Ji, and Chen Huowang. DC/P - A proof assistant for interval logics. Journal of Software, China, 1999.

 [13]

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.

 [14]

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.

 [15]

Catalin Dima. Automata and regular expressions for real-time languages. In Proc. of AFL'99 (9th International Conference on Automata and Formal Languages) Vasszecseny, Hungary, August 1999.

 [16]

Catalin Dima. Kleene theorems for event-clock automata. In Proc. of 12th International Symposium on Fundamentals of Computation Theory, Iasi, Romania, volume 1684 of LNCS, pages 215-225, August 1999.

 [17]

Tran Van Dung and He Jifeng. A Theory of Combinational programs. Technical Report 162, UNU/IIST, P.O.Box 3058, Macau, April 1999.

 [18]

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 Multi-lingual Script Processing.

 [19]

Myatav Erdenechimeg and Richard Moore. Multi-directional Multi-lingual Script Processing. In Proceedings of the Seventeenth International Conference on the Computer Processing of Oriental Languages, Vol. 1, Hong Kong, April 2 - 4, 1997, Oriental Languages Computer Society, Inc, pages 29 - 34, 1997.

 [20]

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.

 [21]

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.

 [22]

Myatav Erdenechimeg, Richard Moore, and Yumbayar Namsrai. On the Specification of the Display of Documents in Multi-lingual Computing. In Ethan V. Munson, Charles Nicholas, and Derick Wood, editors, Principles of Digital Document Processing, volume 1481 of Lecture Notes in Computer Science, pages 70-81. Springer Verlag, 1998.

 [23]

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. To be presented at the 16th International Unicode Conference, Amsterdam, The Netherlands, 27-30 March 2000, under the title Encoding and Implementation Issues in Standardising Traditional Mongolian Script.

 [24]

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.

 [25]

Chris George. Proving Safety of an Authentication Protocol: a Minimal Approach. Technical Report 154, UNU/IIST, P.O.Box 3058, Macau, February 1999.

 [26]

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.

 [27]

Wang Hanpin and Xu Qiwen. Temporal Logics over Infinite Intervals. Technical Report 158, UNU/IIST, P.O.Box 3058, Macau, March 1999.

 [28]

He Hua. A Prettyprinter for the RAISE Specification Language. Technical Report 150, UNU/IIST, P.O.Box 3058, Macau, December 1998.

 [29]

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.

 [30]

Dang Van Hung and Zhou Chaochen. Probabilistic Duration calculus for Continuous Time. Research Report 25, UNU/IIST, P.O.Box 3058, Macau, May 1994. Presented at NSL'94 (Workshop on Non-standard Logics and Logical Aspects of Computer Science, Kanazawa, Japan, December 5-8, 1994). Published in Formal Aspects of Computing (1999) 11: 21-44.

 [31]

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.

 [32]

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.

 [33]

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.

 [34]

Tomasz Janowski and Mathai Joseph. Dynamic Scheduling in the Presence of Faults: Specification and Verification. Research Report 66, UNU/IIST, P.O.Box 3058, Macau, March 1996. Published in the Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996, LNCS 1135, 279-297. Revised paper Dynamic Scheduling and Fault-Tolerance: Specification and Verification is going to appear in Journal of Real-Time Systems Kluwer.

 [35]

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.

 [36]

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.

 [37]

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.

 [38]

Tomasz Janowski and Wojciech Mostowski. Fail-Stop Software Components by Pattern Matching. Technical Report 164, UNU/IIST, P.O.Box 3058, Macau, May 1999. Workshop on Run-Time Result Verification, part of the Federated Logic Conference, Trento, Italy, July 1999. Workshop proceedings available at http://afrodite.itc.it:1024/+AH4-leaf/rtrv.html.

 [39]

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.

 [40]

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.

 [41]

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

 [42]

He Jifeng. A common framework for Mixed Hardware/Software Systems. In the 1st international on Integrated Formal Methods Conference, York, U.K., 28-29 June, 1999. Key Note of IFM Conference.

 [43]

He Jifeng. Integrating Variants of DC. Research Report 172, UNU/IIST, P.O.Box 3058, Macau, August 1999.

 [44]

He Jifeng. Weakest Completion. In IFIP 2.3 Working Group Workshop, Udine, Italy, July 1999.

 [45]

He Jifeng and C.A.R. Hoare. A trace model for pointers and objects. In M. Broy, editor, Lecture Notes of Marktoberdorf International Summer School, ECOOP'99, Germany, August 1999.

 [46]

He Jifeng and C.A.R. Hoare. Linking Theories in Probabilistic Programming. Information Science, 119:205-218, 1999.

 [47]

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.

 [48]

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.

 [49]

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. Accepted for publication by Chinese Journal of Advanced Software Research.

 [50]

Zhan Naijun. Another Formal Proof for Deadline Driven Scheduler. Technical Report 169, UNU/IIST, P.O.Box 3058, Macau, August 1999.

 [51]

Zhan Naijun. Completeness of Higher-Order Duration Calculus. Technical Report 175, UNU/IIST, P.O.Box 3058, Macau, August 1999.

 [52]

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

 [53]

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.

 [54]

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.

 [55]

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.

 [56]

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.

 [57]

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.

 [58]

Margaret Stuart and Zhou Chaochen. UNU/IIST Annual Report 1998. Administrative Report 157, UNU/IIST, P.O.Box 3058, Macau, February 1999.

 [59]

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).

 [60]

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.

 [61]

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.

 [62]

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.

 [63]

Vladimir Zadorozhny. Orthogonal Formalisation of CORBA. Technical Report 121, UNU/IIST, P.O.Box 3058, Macau, August 1997.

 [64]

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

Annual Report 1999

Contents