home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / comp / sys / transput / 1373 < prev    next >
Encoding:
Internet Message Format  |  1993-01-08  |  13.3 KB
  1. Xref: sparky comp.sys.transputer:1373 comp.realtime:1526 comp.specification:610 comp.specification.z:522
  2. Newsgroups: comp.sys.transputer,comp.realtime,comp.specification,comp.specification.z
  3. Path: sparky!uunet!gatech!paladin.american.edu!darwin.sura.net!tulane!alan!mwm
  4. From: mwm@alan.math.tulane.edu (Michael Mislove)
  5. Subject: Reposting of Z and CSP Short Course Announcements
  6. Nntp-Posting-Host-[nntpd-13584]: alan.math.tulane.edu
  7. Message-ID: <1993Jan8.204424.13675@cs.tulane.edu>
  8. Keywords: Formal methods, specification
  9. Sender: news@cs.tulane.edu
  10. Organization: Mathematics Department, Tulane University, New Orleans, LA  70148
  11. Date: Fri, 8 Jan 1993 20:44:24 GMT
  12. Lines: 342
  13.  
  14.  
  15.    This is a reposting of the announcement that Formal Systems, Ltd. will be
  16. offering short courses on Z and on CSP at Tulane University this April.  There
  17. are three new points to note:
  18.    (1) A reduced rate is available for those who participate in both courses.
  19.        Also, an academic rate has now been established for the courses.
  20.    (2) We are asking that those who intend to take either of the courses
  21.        pre-register by March 1.
  22.    (3) Our apologies for the inconvenience, but news etiquette prevents our
  23.        posting the course fees.  Anyone wanting this information should send
  24.        email to: mwm@tulmath.math.tulane.edu
  25.  
  26. A description of both courses follows.
  27.  
  28. ===========================================================================
  29.  
  30.                     Formal Systems (Europe), Ltd
  31.  
  32.                         Course Announcement I:  
  33.  
  34.                      Formal Development Using Z
  35.                        A Tool-Based Course
  36.  
  37.  
  38.                         April 5 - 9, 1993 
  39.                         Tulane University
  40.                     New Orleans, Louisiana USA
  41.  
  42.  
  43.                         Course Lecturer:  
  44.                         J.C.P. Woodcock
  45.  
  46.  
  47. Formal Systems (Europe) Ltd exploits pioneering work in the field of
  48. Formal Methods. The directors and staff include key current and former
  49. members of the Programming Research Group at Oxford University,
  50. England, each with an established international reputation. The company
  51. has extensive industrial experience of the pragmatic application of
  52. formal techniques to the analysis and design of both software and
  53. hardware systems, in Europe and the USA.
  54.  
  55. Since its formation in 1989, Formal Systems has doubled in staff and in
  56. turnover each year. Past and present clients for consultancy include
  57. Inmos Ltd on VLSI design quality assurance, Deutsche System Technik on
  58. formal specification, C.S. Draper Laboratory on fault-tolerant
  59. processors, and Secure Information Systems Ltd on formal verification.
  60. Additionally, Formal Systems is a collaborator in European Community
  61. ESPRIT activities and has given specialized industrial short courses in
  62. conjunction with Oxford University in the UK and Tulane University in
  63. the USA. In 1991 Formal Systems received a prestigious SMART Award from
  64. the UK Department of Trade and Industry for technological innovation in
  65. an aerospace engineering application.
  66.  
  67. Z is a specification language based on mathematical set theory and
  68. logic. It was developed at Oxford University for use in the
  69. specification of state-based programs, and has now matured into a
  70. valuable and widely used development tool.  For example, IBM UK
  71. Laboratories at Hursley have used  Z  to develop approximately 48,000
  72. lines of new code for the CICS system (the main IBM System/370 on-line
  73. transaction processing system).  They obtained a significant reduction
  74. in the volume of software quality defects for ultimately little
  75. additional development cost.  For this achievement, IBM UK Laboratories
  76. and Oxford University Computing Laboratory (PRG) were jointly presented
  77. with a prestigious Queen's Award for Technological Achievement in
  78. 1992.  Z has proved itself to be especially useful as a tool for
  79. formally verifying and demonstrating the correctness of safety critical
  80. and/or secure systems.
  81.  
  82. Objectives:  We present the Z notation, together with systematic
  83. techniques for developing designs and code from Z specifications.
  84. Mechanical assistance in managing specification and proof will be
  85. demonstrated using a mechanical proof assistant .
  86.  
  87. An understanding of elementary logic and set theory is useful.
  88.  
  89.                         Program
  90.  
  91. Lectures and tutorials will cover the following topics:
  92.  
  93. - Logic. Sets, relations and functions, sequences. Mathematical toolkit.
  94.  
  95. - Schemas and schema operations. Using schemas to structure specifications.
  96.  
  97. - Data refinement. Operation refinement. Program development.
  98.  
  99. - Methods of proof. The mechanization of proofs.
  100.  
  101. - Case studies, workshop exercises.
  102.  
  103. - The role of formal methods in software development.
  104.  
  105. Dr J. C. P. Woodcock is Director of External Studies at Oxford
  106. University Computing Laboratory, as well as being a Director of Formal
  107. Systems. His research interests include specification, refinement and
  108. proof of sequential and concurrent systems, security, and technology
  109. transfer.  He has been a consultant for IBM for the last six years
  110. working on formally specifying and analyzing the CICS system.  As a
  111. consultant to IBM for six years, he was a key member of the team who
  112. won the Queen's Award (see above) for specifying and analyzing the CICS
  113. system.  He has taught courses in formal methods to over 1500 students
  114. from industry and academia.
  115.  
  116. Location        Tulane University
  117.         New Orleans, LA
  118.  
  119. Date            April  5 - 9,  1993
  120.  
  121. Duration        Four and a half days
  122.         (ends lunchtime Friday)
  123.  
  124. Course Fee      $xxxx per person includes course materials, lunches and 
  125.                 a course dinner.  Inquire for block rates.
  126.  
  127. Accommodation   Hotel accommodation is available for $xx/night plus tax.       
  128.                 Alternatively, a list of hotels can be supplied on request.
  129.  
  130. Contact         Professor Michael Mislove
  131.         Department of Mathematics 
  132.                 Tulane University 
  133.                 New Orleans, LA  70118 
  134.                 (504) 865-5727
  135.             (mwm@tulmath.math.tulane.edu)
  136.  
  137.  
  138.                           Booking Form
  139.  
  140.                    Formal Development Using Z 
  141.                        April  5-9,  1993
  142.  
  143.  
  144. Number of participants : ______
  145.  
  146. Name
  147.  
  148. ____________________________________________________________________
  149.  
  150.  
  151. ____________________________________________________________________
  152.  
  153. Accommodation Required (Give Dates)
  154.  
  155. ____________________________________________________________________
  156.  
  157.  
  158. ____________________________________________________________________
  159.  
  160. Contact address:
  161.  
  162. ____________________________________________________________________
  163.  
  164.  
  165. ____________________________________________________________________
  166.  
  167.  
  168. Phone:________________________
  169.  
  170. Bookings should be made as soon as possible.
  171.  
  172. Course fee: A deposit of $xxx is required with order (deadline: March 1, 1993).  
  173.             Balance is due by March 31, 1993.
  174.  
  175. Formal Systems (Europe) Ltd. and Tulane University reserve the right to
  176. cancel the course prior to March 31st if it is undersubscribed.
  177.  
  178. ===============================================================================
  179.  
  180.  
  181.                    Formal Systems (Europe), Ltd
  182.  
  183.  
  184.                       Course Announcement II:
  185.  
  186.                        Introductory CSP
  187.                       A Tool-Based Course
  188.  
  189.  
  190.                      April 12 - 16, 1993
  191.                       Tulane University
  192.                     New Orleans, Louisiana
  193.  
  194.  
  195.           Course Lecturers: A.W. Roscoe and G.M. Reed
  196.  
  197.  
  198. Formal Systems (Europe) Ltd. exploits pioneering work in the field of
  199. Formal Methods. The directors and staff include key current and former
  200. members of the Programming Research Group at Oxford University,
  201. England, each with an established international reputation. The company
  202. has extensive industrial experience of the pragmatic application of
  203. formal techniques to the analysis and design of both software and
  204. hardware systems, in Europe and the USA.
  205.  
  206. Since its formation in 1989, Formal Systems has doubled in staff and in
  207. gross income each year. Past and present clients for consultancy
  208. include Inmos Ltd on VLSI design quality assurance, Deutsche System
  209. Technik on formal specification, C.S. Draper Laboratory on
  210. fault-tolerant processors, and Secure Information Systems Ltd on formal
  211. verification.  Additionally, Formal Systems is a collaborator in
  212. European Community ESPRIT activities and has given specialized
  213. industrial short courses in conjunction with Oxford University in the
  214. UK and Tulane University in the USA. In 1991 Formal Systems received a
  215. prestigious SMART Award from the UK Department of Trade and Industry
  216. for technological innovation in an aerospace engineering application.
  217.  
  218. Communicating Sequential Processes (CSP) is a notation for the
  219. specification, design, and analysis of concurrent and distributed
  220. systems.  The theory and application of CSP as an analytical tool has
  221. been developed over the past fifteen years by European academics and
  222. industry.  Furthermore, CSP has been implemented in the form of occam*
  223. and the Transputer.  It is particularly suited for the verification of
  224. expressive power of CSP allows the representation of most of the usual
  225. descriptions of finite state systems,  such as the state transition
  226. systems, Petri nets, many classes of automation, and -- in some
  227. applications -- languages such as VHDL.
  228.  
  229. The course introduces all the important ideas of CSP, and will bring
  230. participants to the point where they can understand what CSP is and
  231. where it is applicable,  and have the ability to apply it to problems
  232. in their own domain.
  233.  
  234. It is centered around a newly developed software tool (FDR), a product
  235. of Formal Systems. FDR tests for Failures- Divergence Refinement, a
  236. powerful and flexible method based on the standard model of CSP.  This
  237. permits verification of both simple and complex specifications of
  238. systems and also direct comparison of different implementations.  Where
  239. a property fails to hold,  FDR has powerful debugging capabilities to
  240. isolate faulty components.  FDR was originally developed as a result of
  241. collaborative work between Formal Systems and Inmos Ltd as a tool for
  242. verifying VLSI designs.  It is now a general purpose tool for the
  243. design and verification of software and hardware systems.
  244.  
  245. By using FDR, students on the course will see CSP come to life, and
  246. learn to use a tool with the capability of dealing with realistically
  247. sized problems.
  248.  
  249. ___________________________ 
  250.  *occam is a trademark of INMOS Ltd
  251.  
  252.  
  253.                          Program  
  254.  
  255. Lectures and  tutorials will cover the following topics:
  256.  
  257. - Interfaces     - Case Studies         - Safety Properties     
  258. - CSP Laws     - Non-determinism       - Deadlock 
  259. - Refinement    - Timed CSP         - Liveness Properties   
  260. - Comparison with other notations
  261.  
  262. Dr A. W. Roscoe and Dr G. M. Reed are both Directors of Formal Systems
  263. and Senior Faculty in Computation at Oxford University.  Both are
  264. pre-eminent researchers in CSP.  Dr Roscoe was one of the original
  265. developers of the language and its theory.  He is an authority on
  266. deadlock avoidance techniques, and he is the chief designer of FDR.
  267. Dr  Reed is best known for his work on Timed CSP, and now leads a large
  268. group at the University developing methods for using CSP in industry.
  269.  
  270. Dr Roscoe is a University Lecturer at Oxford University and a Fellow of
  271. University College, specializing in the theory of parallel computing
  272. and its applications. He is a co-inventor of the failures model for
  273. CSP, the developer of the standard semantics for  occam, and the
  274. director of the team which produced the occam Transformation System
  275. used in the design of the floating-point Transputer.  He is also a
  276. leading authority on the analysis of deadlock in parallel networks.
  277.  
  278. Dr Reed is a University Lecturer in Computation at Oxford University
  279. and a Fellow of St Edmund Hall. He and Dr Roscoe have developed the
  280. theory of real- time distributed computing based on CSP.  There is
  281. currently a large group at Oxford under his direction devoted to making
  282. this theory of practical use for industrial application.
  283.  
  284.  
  285. Location        Tulane University
  286.         New Orleans, LA
  287.  
  288. Date            April 12-16, 1993
  289.  
  290. Duration        Four and a half days
  291.         (ends lunchtime Friday)
  292.  
  293. Course Fee      $xxxx per person Includes course materials, lunches and 
  294.                 a course dinner.  Inquire for block rates.
  295.  
  296.  
  297. Accommodation   Hotel accommodation is available for $xx/night plus tax.  
  298.         Alternatively, a list of hotels can be supplied on request.
  299.  
  300.  
  301. Contact     Professor Michael Mislove
  302.         Department of Mathematics 
  303.         Tulane University 
  304.         New Orleans, LA  70118 
  305.         (504) 865-5727
  306.         (mwm@tulmath.math.tulane.edu)
  307.  
  308.  
  309.                          Booking Form
  310.  
  311.                       Introductory CSP 
  312.                      April 12-16, 1993
  313.  
  314.  
  315. Number of participants : ______
  316.  
  317. Name
  318.  
  319. ____________________________________________________________________
  320.  
  321.  
  322. ____________________________________________________________________
  323.  
  324. Accommodation Required (Give Dates)
  325.  
  326. ____________________________________________________________________
  327.  
  328.  
  329. ____________________________________________________________________
  330.  
  331. Contact address:
  332.  
  333. ____________________________________________________________________
  334.  
  335.  
  336. ____________________________________________________________________
  337.  
  338.  
  339. Phone:________________________
  340.  
  341. Bookings should be made as soon as possible.
  342.  
  343. Course fee: A deposit of $xxx is required with order (deadline March 1).  
  344.             Balance is due by March 31, 1993.
  345.  
  346. Formal Systems (Europe) Ltd. and Tulane University reserve the right to
  347. cancel the course prior to March 31st if it is undersubscribed.
  348.  
  349.  
  350.  
  351.  
  352.  
  353.  
  354.  
  355.  
  356.