_________________ _____________________________________ Table of Contents: > AMAST Newsletter, Sample Issue 01 < ^~~~~~~~~~~~~~~~^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ________ [1] AMAST results: ~~~~~~~~~~~~~ [1.1] Theories and Experiences for Real-Time System Development, Teodor Rus & Charles Rattray (Ed's), AMAST Series in Computing, 2 (December 1994) [1.2] Research report: Verification of an Audio Control Protocol, by Doeko Bosscher, Indra Polak & Frits Vaandrager (CWI) [1.3] Theoretical Computer Science 140:1 (March 1995) Special Issue AMAST'93 ________ [2] Jobs: ~~~~ [2.1] Visiting assistant professor, Computer Science, Pensacola (Florida, USA) [2.2] PhD Studentship in Computational Logic, City Univ. of London (England) [2.3] Post-Doc for women at Univ. Kentucky, Lexington (Kentucky, USA) ________ [3] 7th Int'l Conf. Formal Description Techniques (FORTE'94) : Prel. Program ________ [4] Contents of AMAST ftp repository at CS Faculty of University of Twente _______________________________________________________________________________ emailed: \ / put together by: G. Scollo on: 06 August 1994 \ AMAST Newsletter / thanks to contributions by: to: 142 subscribers / Sample Issue 01 \ [1.1] T. Rus & C. Rattray ^~~~~~~~~~~~~~~~~~^ / \ [1.2] Frits Vaandrager _____________________ ^^^^^^^^^^^^^^^^^^^^^^^^ [2.1-2] COLIBRI 31a Send your comments to: amast@cs.utwente.nl [2.3] Judy Goldsmith _________________ [3] Dieter Hogrefe List subscription: amast-request@cs.utwente.nl [4] the UT CS Helpdesk ^~~~~~~~~~~~~~~~^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ _______________________________________________________________________________ Note: Sample Issue 00 (plain text) can be retrieved by anonymous ftp at URL: ftp://ftp.cs.utwente.nl/pub/doc/amast/newsletter/SampleIssue00 [1.1] ============================================= AMAST News, Sample Issue 01 New book: Theories and Experiences for Real-Time System Development Teodor Rus & Charles Rattray (Editors), AMAST Series in Computing, Vol. 2, World Scientific Pu. Co. (December 1994) Real-time applications bring forth new and intriguing problems regarding program specification, verification and development, and these have motivated intensive programs of research over the last decade. It is time to consider what has been achieved and how to progress from this point. To consider the AMAST perspective on real-time systems, a 1st AMAST Workshop on Real-Time Systems was held in Iowa City, in November 1993. All the Workshop speakers, leading players in the area, were invited. All the authors had the opportunity to refine their papers as a result of the lively discussions that took place during the Workshop. A tangible product of this procedure is the present volume. It is more than simply a proceedings, if only for the fact that there was much more collaborative effort involved in the preparation of the final chapters of this book than normal for usual proceedings. The resulting contents are listed below. A series of further workshops on real-time systems is planned and it is hoped that these will lead to a Handbook on Real-Time System Development in the AMAST Series in Computing. 1 Real-time system = discrete system + clock variables (R Alur & TA Henzinger) 2 Real-time CSP (J Davies & S Schneider) 3 Visual tools for verifying real-time systems (J S Ostroff) 4 Designing supervisors for real-time systems (D Ionescu) 5 Real-time symbolic model-checking (S V Campos & E M Clarke) 6 Verification of an audio control protocol (D Bosscher, I Pollak & F Vaandrager) 7 Approximations for verifying timing properties (H Wong-Toi & D L Dill) 8 A Timed Full LOTOS with Time/Action Tree Semantics (T Bolognesi & F Lucidi) 9 A Timed LOTOS extension (J Quemada, C Miguel, D de Frutos & L Llana) 10 Status-oriented telephone service specification (B Stepien & L Logrippo) 11 Experimenting with LOTOS in the aerospace industry (H Garavel & RP Hautbois) 12 Performance analysis and true concurrency semantics (E Brinksma, JP Katoen, R Langerak & D Latella) 13 State machines, temporal logic and algebraic data models (A Gabrielian) 14 An experiment in developing real-time systems using Mec (D Begay, J Dormoy & P Felix) [1.2] ============================================= AMAST News, Sample Issue 01 Research report Verification of an Audio Control Protocol by Doeko Bosscher, Indra Polak & Frits Vaandrager (CWI) The following CWI report is now available by anonymous ftp from ftp.cwi.nl as the file /pub/CWIreports/AP/CS-R9445.ps.Z : Authors: Doeko Bosscher, Indra Polak and Frits Vaandrager Title: Verification of an Audio Control Protocol Status: Report CS-R9445, CWI, Amsterdam, July 1994. To appear in T. Rus and C. Rattray, editors, Theories and Experiences for Real-Time System Development, 1994. An extended abstract will appear in Proceedings Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT'94), Luebeck, Germany, September 1994, LNCS. Springer-Verlag, 1994. This paper received the ``Best paper of FTRTFT'94 award''. Abstract: We analyze a simple version of a protocol developed by Philips for the physical layer of an interface bus that connects the various devices of some stereo equipment (tuner, CD player,...). The protocol, which uses Manchester encoding, has to deal with a significant uncertainty in the timing of events, due to both hardware and software constraints. We present a formal specification of the protocol, and a proof of correctness for the case where the tolerance of the clocks used within the system is less than $\frac{1}{17}$. A counterexample shows that the protocol fails for tolerances greater than or equal to this value. The verification is carried out using a model of linear hybrid systems, which is similar to the phase transition system model of Manna and Pnueli, and the model of linear hybrid automata of Alur, Henzinger and Ho. The semantics of linear hybrid systems is defined via a translation to the timed I/O automata model of Lynch and Vaandrager. [1.3] ============================================= AMAST News, Sample Issue 01 Theoretical Computer Science 140:1 (March 1995) Special Issue AMAST'93 (G. Scollo and T. Rus, guest editors) The papers in this issue are revised and extended versions of communications presented at the Third International Conference on Algebraic Methodology and Software Technology, held on June 21--25, 1993, at the University of Twente, Enschede, The Netherlands. Among the objectives of the conference, were: to consolidate and expand the trend created by the international dialogue established by the previous two AMAST conferences, and to make a new step toward transforming algebraic methodology into software technology. The six papers selected for this issue testify to the successful achievement of the objectives of the conference. The topics they address are diverse; the approaches, problems and results they propose are novel and, though seemingly unconnected, together they yield a coherent enrichment of the potential of using algebraic methods in the science and technology of computing. D. Pigozzi and A. Salibra Lambda abstraction algebras: representation theorems F. Laroussinie, S. Pinchinat and Ph. Schnoebelen Translations between modal logics of reactive systems R. Gorrieri, M. Roccetti and E. Stancampiano A theory of processes with durational actions A. Mokkedem and D. Mery On using temporal logic for refinement and compositional verification of concurrent systems M. Navarro, F. Orejas and A. Sanchez On the correctness of modular systems E.G. Wagner, On the role of memory in object-oriented languages [2.1] ============================================= AMAST News, Sample Issue 01 Job announcement VISITING ASSISTANT PROFESSOR (non-tenure track) - Ph.D. in Computer Science or closely related field to teach at the main campus in Pensacola. Must be able to teach a variety of computer science courses at the undergraduate and graduate levels. Although the emphasis for this position is on teaching, the successful applicant will be encouraged to become involved in research underway in the department and in the Institute for Human and Machine Cognition. Salary range: $35,000-$40,000. Applicants must provide documentation of the right to work in the United States. Applicants should send a resume, a list of three references, a statement of interests and goals, and a list of specific courses applicant is qualified to teach (all by hard-copy, not e-mail) to Dr. Ed Rodgers, Chair, Department of Computer Science, University of West Florida, Pensacola, Florida 32514. Screening of applications will begin May 1, 1994 and will continue until position is filled. UWF is an equal opportunity/affirmative action employer. [2.2] ============================================= AMAST News, Sample Issue 01 Job Announcement PhD Studentship offered in Computational Logic Department of Computer Science School of Informatics City University, London, UK Applications are invited for a PhD Studentship in the field of Computational Logic, tenable at the department of Computer Science, City University. Areas of particular research interest within this field are: -- concurrent systems: specification and construction -- parallel logic programming -- constraint logic programming -- programming environments -- program analysis, synthesis and transformation -- design of logic programming languages -- logic-based formal description techniques The School of Informatics which has developed a flourishing research base is funding a scheme for awarding research studentships leading to a PhD. These Centenary Studentships are normally awarded for three years and will cover maintenance in line with SERC research studentships as well as tuition fees. Awards for the year 1993/94 are typically in the region of 5,500 pounds sterling. Applicants should contact Dr David Gilbert directly at the address below ------------------------------------------------------------------------------- Dr David Gilbert tel: +44-71-477-8444 (direct/answerphone) Department of Computer Science fax: +44-71-477-8587 School of Informatics City University email: drg@cs.city.ac.uk Northampton Square uucp : drg@citycs.uucp London EC1V 0HB UK ------------------------------------------------------------------------------- [2.3] ============================================= AMAST News, Sample Issue 01 Post-Doc for women at Univ. Kentucky, Lexington (Kentucky, USA) The VP for research and grad studies has just announced postdocs for women in engineering, life and physical sciences. (CS just moved to engineering this summer, so that includes us). The postdocs will be for up to 2 years, starting as early as this fall. * This for women who are US citizens or permanent residents, * have a PhD by the beginning of the postdoc, and not for more than 2 years. * The pay is $25K/year plus $5K research support. You need a faculty mentor. I do structural complexity + a (very) little bit of computational geometry; there is another computational geometry and algorithms person, and cryptography, logic programming, db, systems, graphics/3D vision, numerical analysis, .... The application is a cv, 3 letters of recommendation, sample publications or dissertation chapters, a research proposal, and a letter from the proposed mentor. UK is in Lexington, KY, a pleasant small city on I75 and I64, between Cincinnati (80 miles to the north) and Knoxville (170 miles to the south). It is a friendly city with beautiful tree-lined residential streets, and a leisurely pace of life. judy goldsmith goldsmit@cs.uky.edu 606-257-4245 [3] =============================================== AMAST News, Sample Issue 01 FORTE'94, Seventh International Conference on FORMAL DESCRIPTION TECHNIQUES Berne, Switzerland, 4 - 7 October 1994. PRELIMINARY PROGRAM is available. FORTE'94 will be held in Berne, in the "Aula" of the main building of the University of Berne, Hochschulstr. 4, CH-3012 Berne, Switzerland, 4 - 7 October 1994. Conference rooms are wheel-chair accessible. Please indicate on the registration form whether you need special help. The conference offers the presentation of 24 research papers, 3 industrial usage reports, 12 position statements, 6 tutorials and a number of tool demonstrations. Tutorials will be held on October 4 only. Tool presentations will take place concurrently with conference presentations on October 5 to 7. FORTE'94 will address formal techniques applicable to Distributed Systems such as Estelle, Lotos, SDL, ASN.1, Automata, Logics, Process Algebras, etc., and will include industrial applicability to Protocols and Distributed Systems. The conference will be a forum for presentation of the state of the art in theory, application, tools and industrialization of Formal Techniques and will provide an excellent orientation for newcomers. FORTE'94 will be sponsored by IFIP WG6.1 in cooperation with ACM SIGCOMM and the IEEE Computer Society Technical Committee on Distributed Processing. Additional supporters are: Alcatel STR, Siemens-Albis, ASCOM, Sun Microsystems and Swiss Telecom as well as the non-corporate sponsors Beer-Brawand Fund and the Swiss National Science Foundation. Participants will receive participants' proceedings and tutorial notes, the final proceedings will be published by Chapman & Hall, official publisher of IFIP WG6.1 proceedings, in early 1995. Further Information: FORTE'94 Organization Committee, University of Berne, P.O. Box 900, CH-3000 Berne 9, Switzerland Email: forte94@iam.unibe.ch. To obtain additional information and latest news please login via ftp on host `siam.unibe.ch' (IP address 130.92.66.11) as user `anonymous' and give your email address as password, then get the appropriate file from directory `forte94' (for particular filenames see file `README'). [4] =============================================== AMAST News, Sample Issue 01 _________________________________________________________________________ Description of AMAST ftp repository at CS Faculty of University of Twente ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ URL : ftp://ftp.cs.utwente.nl/pub/doc/amast/ Date : 05/08/1994 Contents : README, amast93/, info/, newsletter/, sigala/ README : this page amast93/ : reports on AMAST'93 Conference and on two AMAST Workshops: o Real-Time Systems, Iowa City, Nov. 1-3, 1993 o Topology and Completion in Semantics, Chartres, Nov. 18-20, 1993 all published in the Bulletin of the EATCS Contents : 3rdConfReport.tex, 3rdConfReport.dvi, 3rdConfReport.ps, 1stWRTSReport.tex, 1stWRTSReport.dvi, 1stWRTSReport.ps, 1stWTCSReport.tex, 1stWTCSReport.dvi, 1stWTCSReport.ps info/ : digest of contributions to discussion on a proposed AMAST newsletter, new AMAST mailing lists and communication styles Contents : Digest01 [29/07/1994; next digest expected mid-August] newsletter/ : sample issues of a proposed AMAST newsletter Contents : SampleIssue00 [29/07/1994; next issue not planned yet] sigala/ : first two issues of the SIGALA Newsletter Contents : snl94001.ps, snl94002.tex, snl94002.dvi, snl94002.ps [end] ============================================ AMAST News, Sample Issue 01