A specification case study.

• To: larch-interest@PA.DEC.COM
• Subject: A specification case study.
• From: KURODA Kiyotaka <kuroda@cs.cmu.edu>
• Date: Mon, 31 Jul 95 09:07:08 -0400
• Cc: kuroda@cs.cmu.edu
• Delivery-Date: Mon, 31 Jul 95 06:19:28 -0700
• Sender: Kiyotaka_Kuroda@VACHE.VENARI.CS.CMU.EDU

Dear Fellow Larch specifiers and provers,

I am an engineer from Mitsubishi Electric Corporation (Yokohama,
Japan) and have been visiting Jeannette Wing at Carnegie Mellon for
almost a year.  I have been busy specifying a device type hierarchy in
Larch and proving properties about the types using LP.  (The subtype
notion is based on Liskov and Wing's behavioral notion of subtyping.)

I would like to share with you my experience in writing specifications
and doing proofs in LP.  I have just created a home page for my
specification case study:

http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kuroda/WWW/devSpec/deviceModels.html

which has links to the LSL and LCL specifications and LP proofs.
Feel free to browse.  Your comments are welcome!

Kiyotaka Kuroda

• Prev: FWD: Dagstuhl specification competition, reactive control systems
• Next: FWD: CFP for Formal Methods Europe
• Index: Larch archive index