Annual Report 1998

Contents

References

 [1]

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), LNCS 1486, pp. 241-250, Springer-Verlag, 1998.

 [2]

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.

 [3]

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

 [4]

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.

 [5]

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), LNCS 1486, pp. 282-293, Springer-Verlag, 1998.

 [6]

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.

 [7]

Pablo Giambiagi. Verification of the STARI Circuit in Duration Calculus. Technical Note DeTfoRS 13, UNU/IIST, P.O.Box 3058, Macau, March 1998. To be published as UNU/IIST report.

 [8]

Pablo Giambiagi and Gerardo Schneider. Modelling and simulation the STARI circuit in Verilog. Technical Note DeTfoRS 14, UNU/IIST, P.O.Box 3058, Macau, March 1998. To be published as UNU/IIST report.

 [9]

Wang Hanpin and Xu Qiwen. A Complete Logic Over Infinite Intervals. Technical Note DeTfoRS 18, UNU/IIST, P.O.Box 3058, Macau, October 1998. To be published as UNU/IIST report.

 [10]

Hu Chengjun. DC/P: A Proof Assistant for Interval Logics. Technical Note DeTfoRS 16, UNU/IIST, P.O.Box 3058, Macau, October 1998. To be published as UNU/IIST report.

 [11]

Hu Chengjun. DC/P User's Guide. Technical Note DeTfoRS 17, UNU/IIST, P.O.Box 3058, Macau, October 1998. To be published as UNU/IIST report.

 [12]

Catalin Dima. Timed Regular Expressions, Real-time Automata and Simple Duration Calculus. Technical Note DeTfoRS 15, UNU/IIST, P.O.Box 3058, Macau, October 1998. To be published as UNU/IIST report.

 [13]

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.

 [14]

Dimitar P. Guelev. Iteration of Simple Formulas in Duration Calculus. Technical Report 141, UNU/IIST, P.O.Box 3058, Macau, June 1998.

 [15]

Dimitar Guelev. Probabilistic Interval Temporal Logic. Technical Report 144, UNU/IIST, P.O.Box 3058, Macau, August 1998.

 [16]

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

 [17]

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.

 [18]

Chris George and Xia Yong. An Operational Semantics for Timed RAISE. Technical Report 149, UNU/IIST, P.O.Box 3058, Macau, November 1998.

 [19]

Dimitar P Guelev. Quantification over State in Duration Calculus is Essentially First Order. Technical Note DeTfoRS 11, UNU/IIST, P.O.Box 3058, Macau, July 1998. To be published as UNU/IIST report.

 [20]

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), LNCS 1486, pp. 186-197, Springer-Verlag, 1998.

 [21]

Suman Roy and Zhou Chaochen. Notes on Neighborhood Logic. Research Report 97, UNU/IIST, P.O.Box 3058, Macau, February 1997.

 [22]

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.

 [23]

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.

 [24]

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.

 [25]

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), LNCS 1486, pp. 55-64, Springer-Verlag, 1998.

 [26]

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.

 [27]

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

 [28]

Zheng Tao and Li Xuandong. Hybrid Regular Expressions. In Hybrid Systems 98, Berkely, April 13-15 1998. Springer-Verlag. The work done by the UNU/IIST off-shore research project at Nanjing University.

 [29]

Zhou Chaochen. Reorganisation of Duration Calculi. In Michael R. Hansen, editor, ESSLLI'98 workshop on Duration Calculus: A Logical Approach to Real-Time Systems, August 24-28 1998.

 [30]

Gao Jianping and Chen Zongji. Formal Development of a Feedback Control System with Fault Accommodation. In Michael R. Hansen, editor, ESSLLI'98 workshop on Duration Calculus: A Logical Approach to Real-Time Systems, pages 41-50, August 24-28 1998.

 [31]

Qiu Zongyan. A Logic for Super-Dense Computation. In Michael R. Hansen, editor, ESSLLI'98 workshop on Duration Calculus: A Logical Approach to Real-Time Systems, pages 151-159, August 24-28 1998.

 [32]

Wang Ji. A Superdense Duration Semantics for Hybrid Systems. In Michael R. Hansen, editor, ESSLLI'98 workshop on Duration Calculus: A Logical Approach to Real-Time Systems, pages 141-150, August 24-28 1998.

 [33]

Rana Barua, Qiu Zongyan, and Zhou Chaochen. Weak Completeness of a Combination of Neighbourhood Logic and Temporal Logic. In Michael R. Hansen, editor, ESSLLI'98 workshop on Duration Calculus: A Logical Approach to Real-Time Systems, pages 5-12, August 24-28 1998.

 [34]

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.

 [35]

Tomasz Janowski, Rumel V. Atienza, and Gustavo Gimeé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.

 [36]

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: February 1999.

 [37]

Tomasz Janowski, Zheng Hongjun, and Gustavo Gimenez 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.

 [38]

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.

 [39]

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.

 [40]

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.

 [41]

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.

 [42]

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.

 [43]

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.

 [44]

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.

 [45]

Venkat P Reddy. A First Course in Software Engineering. Technical Report 78, UNU/IIST, P.O.Box 3058, Macau, July 1996.

 [46]

Yu Huiqun. A Course of Formal Methods in Software Development. Technical Report 79, UNU/IIST, P.O.Box 3058, Macau, August 1996.

 [47]

Tan Xinming. Enquiring about Bus Transport-Formal Development using RAISE. Technical Report 83, UNU/IIST, P.O.Box 3058, Macau, September 1996.

 [48]

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.

 [49]

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.

 [50]

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

 [51]

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.

 [52]

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.

 [53]

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.

 [54]

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.

 [55]

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.

 [56]

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

Annual Report 1998

Contents