参考資料・リンク集

■参考資料・リンク集

並行プロセスのモデル化と検証

プロセス代数設計(LOTOS)

形式化数学検証系(MIZAR)

MPI/PCクラスタ並列計算

 

←目次へ戻る

2010年6月17日 18:00 更新

 

●並行プロセスのモデル化と検証

Systems and Software Verification (Model-Checking Techniques and Tools)
Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.
2001, XII, 190 pp. 67 figs., Hardcover ISBN: 3-540-41523-8 , Springer-Verlag

Cellular Automata Machines (A New Environment for Modeling)
Tommaso Toffoli and Norman Margolus
Cloth / April 1987 , ISBN: 0-262-20060-0, The MIT Press

Cellular Automata and Complexity: Collected Papers
Stephen Wolfram, 1994: ISBN 0-201-62716-7, StephenWolfram.com

Petri Nets World
http://www.daimi.au.dk/PetriNets/

Petri Nets : Properties, Analysis and Applications
T.Murata : Proc.IEEE,Vol.77, No.4, pp.541-580 (1989). abstract

Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use , Vol.1, Basic Concepts
KurtJensen, 2nd ed. 1996. 2nd corr. printing, 1997, XII, 234 pp. 84 figs., Hardcover
ISBN: 3-540-60943-1 Springer-Verlag

A Calculus of Communicating Systems
R. Milner, 1982, ISBN:0387102353 , Springer-Verlag

Communicating Sequential Processes
C.A.R. Hoare, Prentice-Hall, 1985.
http://www.usingcsp.com/cspbook.pdf

Model Checking
Edmund M. Clarke, Orna Grumberg and Doron A. Peled
Cloth / January 2000 , ISBN: 0-262-03270-8, The MIT Press


●プロセス代数設計(LOTOS

::Reference definition::

ISO International Standard 8807:1989
Information processing systems - Open Systems Interconnection -
LOTOS - A formal description technique based on the temporal ordering of observational behaviour
Geneva, September 1989
An annex of the LOTOS standard provides a user-friendly tutorial.

::Books and Papers::

Using Formal Description Techniques - An Introduction to ESTELLE, LOTOS, and SDL
Kenneth J. Turner , John Wiley, 1993, 431 pages , ISBN 0-471-93455-0

Introduction to the ISO Specification Language LOTOS
Tommaso Bolognesi and Ed Brinksma
Computer Networks and ISDN Systems 14(1) 25-59, January 1987, 66 pages

::Related Web sites::

World-wide Environment for Learning LOTOS (WELL)
http://www.cs.stir.ac.uk/~kjt/research/well/

University of Twente (The Netherlands)
http://wwwtios.cs.utwente.nl/lotos/

University of Ottawa (Canada)
http://lotos.site.uottawa.ca/ftp/pub/Lotos/

University of Helsinki (Finland)
http://www.cs.helsinki.fi/research/moco/lotos.html


●形式化数学検証系(MIZAR)

Mizarホームページ(Poland)
http://mizar.org/

ミラーサイト(信州大学)
http://markun.cs.shinshu-u.ac.jp/Mirror/mizar.org/

Megrez service
http://megrez.mizar.org/

MIZAR 講義録(改訂第4版) HTML版 (中村研究室作成)
http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar4/index-j.html

Mizarによる証明記述法 (師玉教授)
http://ysserve.cs.shinshu-u.ac.jp/Lecture/Meta/Mizar.html


●MPI/PCクラスタ並列計算

並列計算/HPC 関係リンク集
http://ysserve.cs.shinshu-u.ac.jp/~wasaki/HPC/index-j.html

MPI Forum : MPI(Message Passing Interface) standard :
http://wiht.link/MPIguide

Marc Snir, et.al : MPI: The Complete Reference :
http://www.netlib.org/utk/papers/mpi-book/mpi-book.html

Peter Pacheco : Parallel Programming with MPI :
http://nexus.cs.usfca.edu/mpi/

P.Pacheco著(秋葉訳):MPI並列プログラミング(上記本の邦訳版):培風館
http://www.alde.co.jp/mpi/

 

 

wasaki _AT_ cs.shinshu-u.ac.jp
Copyright(c) Katsumi Wasaki. All rights reserved.