Home Page
forte97
last updated November 19, 1997
 
formalWARE 
    project  

  Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

FORTE/PSTV'97 



 
1997 IFIP TC6/WG6.1 Joint International Conference on
FORMAL DESCRIPTION TECHNIQUES
for Distributed Systems and Communication Protocols, and 
PROTOCOL SPECIFICATION, TESTING, AND VERIFICATION
Osaka, Japan November 18-21, 1997
 
 

 
General Information  

Program  
     Session 1:  Testing Theory for Concurrent Systems 
     Session 2:  MSC and ODP 
     Session 3:  LOTOS and Extension 
     Session 4:  Verification Techniques 
     Session 5:  Conformance Testing 
     Session 6:  Real Time Systems 
     Session 7:  Languages and Applications 
     Session 8:  Industrial Usage Reports 
     Session 9:  Concurrent Systems 

Committee Members 
Conference Registration 
Accomodations 
Travel Agent 
Other Information 
Further Information 
 

General Information  

FORTE/PSTV'97 will address Formal Description Techniques (FDTs) applicable to communication protocols and distributed systems (such as Lotos, SDL, Estelle, ASN.1, TTCN, Z, automata, process algebras, logics). The conference will be a forum for presentation of the state of the art in theory, application, tools and industrialization of FDTs, and will provide an excellent orientation for newcomers. From 1996, the hitherto separate conferences FORTE and PSTV have been combined into a joint edition (FORTE/PSTV). 

The conference offers the presentation of 29 research papers, 4 industrial usage reports, 4 tutorials and a number of tool demonstrations. Invited talks will be given by Henry Chang (IBM T.J. Watson Research Center, USA), Shoichi Noguchi (Aizu Univ., Japan) and Ichiroh Sakakibara (NTT, Japan). Tutorials and tool presentations will be held on November 18. Participants will receive the final proceedings published by Chapman & Hall, the official publisher of IFIP TC6/WG6.1 proceedings, at the conference. 

FORTE/PSTV'97 is organized by Information Processing Society of Japan (IPSJ) and sponsored by IFIP TC6/WG6.1. Corporate supporters are Information Processing Society of Japan (IPSJ) and The Telecommunication Advancement Foundation (TAF). 
 



PROGRAM  

The below is a Preliminary Conference Program.  

Nov. 18 (Tue.), 1997 

Tutorial I--A (9:00--12:00) 
Specification, Proof Checking, and Model Checking for Protocols and Distributed Systems with PVS  
J. Rushby (SRI International, USA) 

Tutorial I--B (9:00--12:00) 
Tutorial on Network Security  
B. Lundy (U S Naval Postgraduate School, USA) 

Tutorial II--A (13:30--16:30) 
A tutorial on E-LOTOS  
A. Jeffrey (Univ. of Sussex, UK) and G. Leduc (Univ. of Liege, Belgium) 

Tutorial II--B (13:30--16:30) 
Object-Oriented Technology for Distributed, Real-Time Systems  
M. Aoyama (Niigata Inst. of Tech., Japan) 
 
Tutorial III (17:00--18:00) 
Tool Demo and Presentation 
 
Nov. 19 (Wed.), 1997 
Registration (8:30-9:00) 
Welcome Address (9:00-9:10) 
Invited Talk I (9:10--10:10) 
 Network and Application for New Generation  
I. Sakakibara (NTT, Japan) 
 
Session 1: Testing Theory for Concurrent Systems (10:30--12:30) 
Specification-based Testing of Concurrent Systems  
A. Ulrich and H. Koenig 

Refusal Testing for Classes of Transition Systems with Inputs and Outputs  
L. Heerink and J. Tretmans 

A Framework for Distributed Object-Oriented Testing  
A.C.Y. Wong, S.T. Chanson, S.C. Cheung and H. Fuchs 
 
Interoperability Test Suite Derivation for Symmetric Communication Protocols  
S. Kang and M. Kim 
 
 
Session 2: MSC and ODP (14:00--16:00) 
A Hierarchy of Communication Models for Message Sequence Charts  
A. Engels, S. Mauw and M.A. Reniers 
 
Timing Constraints in Message Sequence Chart Specifications  
H. Ben-Abdallah and S. Leue 
 
Consistent Semantics for ODP Information and Computational Models  
J. Dustzadeh and E. Najm 
 
Specifying the ODP Trader: An Introduction to E-LOTOS 
G. F. Lucero and J. Quemada 
 

Session 3: LOTOS and Extension (16:30--18:20)  
A Computer Aided Design of a Secure Registration Protocol  
F. Germeau and G. Leduc 
 
Implementation of Distributed Systems described with LOTOS Multi-rendezvous on Bus Topology Networks  
K. Yasumoto, K. Gotoh, H. Tatsumoto, T. Higashino and K. Taniguchi 
 
Disjunction of LOTOS Specifications  
M.W.A. Steen, H. Bowman, J. Derrick and E.A. Boiten 

A Timed Automaton Model for ET-LOTOS Verification  
C. Hernalsteen 
 
 

Nov. 20 (Thu.), 1997 
Session 4: Verification Technique (9:00--10:40) 
Automatic Checking of Aggregation Abstractions Through State Enumeration  
S. Park, S. Das and D.L. Dill 
 
Concept of Quantified Abstract Quotient Automaton and its Advantage  
G. Juanole and L. Gallon 
 
Validating Protocol Composition for Progress by Parallel Step Reachability Analysis  
G. Singh and H. Liu 
 
An Improved Search Strategy for Lossy Channel Systems  
P.A. Abdulla, M. Kindahl and D. Peled 
 
 
Session 5: Conformance Testing (11:10--12:40)  
A Weighted Random Walk Approach for Conformance Testing of a System Specified as Communicating Finite State Machines  
D. Kang, S. Kang, M. Kim and S. Yoo 
 
Friendly Testing as a Conformance Relation  
D. de Frutos-Escrig, L. Llana-Diaz and M. Nunez 
 
Generalized Metric Based Test Selection and Coverage Measure for Communication Protocols  
J. Zhu and S.T. Vuong 
 

Invited Talk II (14:00--15:00) 
The Future Information Technology and its Impact to the Society  
S. Noguchi (Aizu Univ., Japan) 
 
 
Session 6: Real Time Systems (15:00--16:00) 
Dynamic Priorities for Modeling Real-Time  
G. Bhat, R. Cleaveland and G. Luettgen 
 
On-Line Timed Protocol Trace Analysis Based on Uncertain State Descriptions  
M. Musial 
 

Session 7: Languages and Applications (16:30--18:20)  
Algebraic Specification through Expression Transformation  
M.J. Fernandez Iglesias and M. Llamas Nistal 
 
Modelling Digital Logic in SDL  
G. Csopaki and K.J. Turner 
 
A Methodology for the Description of System Requirements and the Derivation of Formal Specifications  
A. Togashi, F. Kanezashi and X. Lu 
 
On the Influence of Semantic Constraints on the Code Generation from Estelle Specifications  
R. Henke, A. Mitschele-Thiel and H. Koenig 
 

Conference Banquet (19:00--21:00)  
at Hotel NEW OTANI OSAKA  
Nov. 21 (Fri.), 1997 
 

Session 8: Industrial Usage Reports (9:00--11:00) 
Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network   
J.H. Andrews, N. A. Day and J.J. Joyce 
 
An Experiment in using RT-LOTOS for the Formal Specification and Verification of a Distributed Scheduling Algorithm in a Nuclear Power Plant Monitoring System  
L. Andriantsiferana, J.-P. Courtiat, R.C. De Oliveira and L. Picci 
 
Intelligent Protocol Analyzer with TCP Behavior Emulation for Interoperability Testing of TCP/IP Protocols  
T. Kato, T. Ogishi, A. Idoue and K. Suzuki 
 
Eight Years of Experience in Test Generation from FDTs using TVEDA  
R. Groz and N. Risser 
 

Invited Talk III (11:30--12:30) 
Distributed Object Consistency in Mobile Environments  
H. Chang (IBM T.J. Watson Research Center, USA) 
 

Session 9: Concurrent Systems (14:00--15:50) 
Self-independent Petri Nets for Distributed Systems  
Y. Sun, S. Liu and M. Ohba 
 
Combining CSP and Object-Z: Finite or Infinite Trace Semantics?  
C. Fischer and G. Smith 
 
Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems  
R. Barbuti, N. De Francesco, A. Santone and G. Vaglini 
 
On a Concurrency Calculus for Design of Mobile Telecommunication Systems  
T. Ando, K. Takahashi and Y. Kato 
 

Panel (16:20--17:50) 
Future FORTE/PSTV  
Panelists will be announced soon 
 
Closing and Farewell (17:50--18:00) 
 



Committee Members   

General Co-Chairs 
Tadanori Mizuno (Shizuoka Univ., Japan),  
Norio Shiratori (Tohoku Univ., Japan 

Organization Committee Co-Chairs 
Kenji Suzuki (KDD, Japan),  
Kenichi Taniguchi (Osaka Univ., Japan) 
 
Program Co-Chairs 
Teruo Higashino (Osaka Univ., Japan),  
Atsushi Togashi (Shizuoka Univ., Japan) 
 
Tutorial Co-Chairs 
Fumiaki Sato (Shizuoka Univ., Japan),  
Ming T. Liu (Ohio State Univ., USA) 
 
Program Committee  
M. Aoyama (Nigata Inst. of Tech., Japan), G. v. Bochmann (Univ. of Montreal, Canada), T. Bolognesi (CNUCE, Italy), E. Brinksma (Univ. of Twente, Netherlands), H. Bowman (Univ. of Kent at Canterbury, UK), S. Budkowski (INT, France), A. Cavalli (INT, France), S. T. Chanson (Univ. of Sci. and Tech., Hong Kong), Y.Choi (Seoul National Univ., Korea), J.-P. Courtiat (LAAS-CNRS, France), R. Dssouli (Univ. of Montreal, Canada), S. Fischer (Univ. of Mannheim, Germany), R. Gotzhein (Univ. of Kaiserslautern, Germany), M. Gouda (Univ. of Texas at Austin, USA), R. Groz (CNET, France), D. Hogrefe (Univ. of Luebeck, Germany), E. Horita (NTT, Japan), Y. Kakuda (Osaka Univ., Japan), M. C. Kim (Korea Telecom, Korea), K. Futatsugi (JAIST, Japan), G. Leduc (Univ. of Liege, Belgium), D. Lee (Bell Lab., USA), S. Leue (Univ. of Waterloo, Canada), L. Logrippo (Univ. of Ottawa, Canada), N. Lynch (MIT, USA), J. de Meer (GMD FOKUS, Germany), E. Najm (ENST, France), N. Nakano (Mitsubishi, Japan), S. Obana (KDD, Japan), K. Ohmaki(ETL, Japan), J. Quemada (ETSI Telecom., Spain), H. Rudin (IBM, Switzerland), B. Sarikaya (Aizu Univ., Japan), R. Tenney (Univ. of Massachusetts, Boston, USA), K. Turner (Univ. of Stirling, UK), S. T. Vuong (Univ. of British Columbia, Canada), J. Wu (Tsinghua Univ., China) 
 
 
 



Conference Registration   

FORTE/PSTV'97 will be held at  
NEC C&C Plaza Hall,  
Shiromi 1--4--24, Osaka, Japan. 
 
Conference registration fees are as follows. 

on or before Sept. 30, 1997  
Regular Registration Fee = 50,000 Yen  
Student Registration Fee = 15,000 Yen 

after Sept. 30, 1997  
Regular Registration Fee = 60,000 Yen  
Student Registration Fee = 20,000 Yen 
 

All fees are in Japanese Yen, payable in advance. Early registration deadline is *Sept. 30, 1997*. Regular Reg. Fee covers: tutorial/conference admission, tutorial notes, final proceedings and conference banquet Student Reg. Fee covers: same as Regular Reg. Fee, except conference banquet Please attach proof of student status (will also be requested at the welcome desk) for Student Reg..  
 



Accommodation Information  

Rooms have been reserved between November 16 and 21, 6 nights at the following hotels.  
HOTEL NEW OTANI OSAKA  
(4 or 5 star hotel : 1 min. walk from conf. site) 

Single = 11,000 Yen  
Twin = 16,500 Yen  
Twin (Single Use) = 13,750 Yen 
 
HOTEL KEIHAN KYOBASHI  
(2 or 3 star hotel : 10 min. walk from conf. site) 

Single = 8,500 Yen 

HOTEL KEIHAN OSAKA  
(2 star hotel : 8 min. train & 10 min. walk from conf. site) 
 
Single = 6,600 Yen 
 
Above all rates are ROOM CHARGE including 10% service charge. Please note that government tax (5%) will be additionally charged to the above amount when you check out at the hotel. Hotel reservations received *after Sept. 30, 1997,* will be accepted on a space available basis only. Note that there are no official hotel ranks in Japan and the above ranks are informal. 
 



Official Travel Agent  
 

Kinki Nippon Tourist Co.,Ltd.(KNT), International Travel, Osaka has been appointed as the official travel agent for the conference. KNT will handle conference registrations as well as hotel reservations for all participants. All correspondence regarding registrations and hotel reservations should be addressed to: 
 
Kinki Nippon Tourist Co., Ltd.  
International Travel, Osaka Branch  
Phone: +81-6-313-6868  
Fax: +81-6-314-1601  

c/o Nikko Bldg. 7F, 2-11-8, Sonezaki, Kita-ku, Osaka 530, JAPAN  
E-Mail: intlosa@tabi.knt.co.jp 
 
Reservations should be made by completing and returning the  
Conference Registration and Hotel Reservation Form  
by FAX or postal mail. To obtain the Form, Please browse our World-Wide Web pages, the URL is 
http://sunfish.ics.es.osaka-u.ac.jp/forte.pstv97/reg.html  
 
You can get the PS, dvi, latex files of the Form from the Web page.  
 



Other Information   
 
Passport & Visa 
All foreign visitors wishing to enter Japan must have a valid passport. Visas will also be required for participants coming from most eastern European countries, the People's Republic China, etc. For further information, participants are recommended to consult their carrier, local travel agencies or the nearest Japanese diplomatic mission. 

Foreign Currency Exchange & Banking 
The local currency is Japanese Yen. Major foreign currencies such as U.S. Dollars, Deutsche Marks, French & Swiss Francs and Pounds Sterling can be changed at the airport or authorized banks. It is possible that you may have trouble in changing money into local currency if you bring other than main international currencies. Banking hours are 9:00 to 15:00, Monday through Friday except National Holidays.  

Note that "1 US $ = 119 Yen" (on Aug. 6, 1997). 
 
Insurance 
All Conference participants are strongly advised to carry the proper travel and health insurance, as the conference committee cannot accept liability for any accidents or injuries that may occur at the Conference. Please consult your travel agent regarding the matter.  
 
 



Further Information  

For further information, please contact 

Program Co-Chair : Prof. Teruo Higashino  
Dept. of Information and Computer Sciences, Osaka University  
Toyonaka, Osaka 560, Japan  
Phone : +81-6-850-6607  
Fax : +81-6-850-6609  
Email : forte-pstv97@ics.es.osaka-u.ac.jp  
To obtain additional information, you may also browse our World-Wide Web pages, the URL is  
 
http://sunfish.ics.es.osaka-u.ac.jp/forte.pstv97 
 



higashino@ics.es.osaka-u.ac.jp