Specialization Track in Software Development through Rigorous Methods





		UPM / IMDEA Track in Software Development through Rigorous Methods Table of Contents Analysis of concurrent systems Coordinator(s)/Instructor(s) Length Prerequisites Course web page (if any) Summary and objectives Topics Evaluation Recommended reading Analysis of concurrent systems Coordinator(s)/Instructor(s) Lars-Åke Fredlund, Clara Benac Length 4 credits (ECTS) Prerequisites Basic finite automaton theory. Acquaintance with concurrent executions and its peculiar characteristics. This course has specific requirements, and if your initial level is not adequate, you may not pass. Therefore, we ask you to please include it in the mail you ought to send to graduate.school (at) software.imdea.org with the list of courses you want to take from the IMDEA track. You will receive a mail stating the courses in which you are welcome to enroll. If you enroll in an IMDEA Track course for which you did not receive explicit approval, you may be asked to switch over to a different one. Course web page (if any) Not yet available. Summary and objectives A pragmatic approach to the analysis of concurrent systems which will give the student a view of different approaches to ensure up to a certain point that a concurrent system is executing as it should. The course will mix lectures, presentations delivered by students (based on assigned reading material), and exercises using a model checker. Topics Concurrent and reactive systems in general. Correctness properties for concurrent systems: short intro to logics like LTL, CTL, Buchi automata, …, etc Testing of concurrent systems. Model checking of concurrent systems. Bounded model checking techniques, and symbolic model checking in general. Intro to hybrid and real-time systems Tools (depending on time and needs during the course): QuickCheck/PropEr SPIN Uppaal McErlang/Java Pathfinder nuSMV etc… Evaluation The grades of the students will be based on the quality and depth of the presentations given by the students and the results of the exercises using a model checker. Recommended reading Will depend on the background of the students. Back to the initial page Go to the IMDEA Software Institute page




Fractals are used with permission from their author Cory Ench \| © 2006-2007. IMDEA Software. All rights reserved \| Legal Notice \| Privacy Policy