[an error occurred while processing this directive]
<meta NAME="ROBOTS" CONTENT="index,follow">
<meta NAME="keywords" CONTENT=" system, course, principles, distributed, student, specification, protocols, concurrent, control, tool, refinement, experience, interference, analysis, modelling, concurrency, testing, gain, communications, understanding, comprehensive, communicating, organisation, particularly, development, combinatorics, observations, abstraction, independence, requirements, objectives, sequential, interaction, challenge, constraints, structure, essential, compression, reasoning, databases, processes, transition, preparation, formalism, realistic, rigorous, practical, registering, strategies, execution, provided, applying, problems, tolerance, explosion, contents, complex, immense, teaches, deadlock, knowledge, livelock, checking, feature, support, planned, timeouts, security, toolset, expected, process, notation, history, context, useful, failure, dealing, design, working, syntax, events, errors, timing, delays, safety, dates, advice, model, media, fault, state">
<meta name="DESCRIPTION" content="Advanced Concurrency Tools: Model Checking course The rigorous development of a complex concurrent or distributed system is an immense challenge for any organisation This course teaches principles of structure and refinement that are particularly useful in understanding such systems An essential feature of this course is the comprehensive tool support that is provided for reasoning about concurrent systems: communications protocols, distributed databases, and control systems ">


<meta name="Edited" content="Sun, 31 Dec 2017 19:20:02 GMT">
<meta name="Published" content="Sun, 31 Dec 2017 19:20:05 GMT">

<title>Software Engineering at Oxford | Advanced Concurrency Tools: Model Checking ( MCH )</title>

<!-- icon -->
<link rel="shortcut icon" type="image/ico" href="../favicon.ico">

<script src="https://ssl.google-analytics.com/urchin.js" type="text/javascript"></script>
<script type="text/javascript">_uacct = "UA-1306673-1";urchinTracker();/*UA-579489-1*/</script>
<META name="verify-v1" content="CwYQSB0rDIbG5v7tQy+2xKxvNEoOxCNSFYYF7mSW7bo=" />
[an error occurred while processing this directive]

<div id="breadcrumb">
   
   <ul class="mainnav">
      <li>
         <a href="/">Computer Science</a></li><li><a href="/softeng/">Software Engineering</a>
      </li>
      <li>
         <a href="/softeng/courses/">Courses</a>
      </li>
      <li>
         <a href="/softeng/courses/subjects.html">Subjects</a>
      </li>
      <li>
         <span class="youarehere">Advanced Concurrency Tools: Model Checking ( MCH )</span>
      </li>
   </ul>
</div>


<!--
<span id="headerItem">
  <a href="../programme/contact.html" title="Contacts">Contact</a> | 
  <a href="../search/search.jsp" title="Search">Search</a> |
  <a href="../sitemap.html" title="Sitemap">Site map</a> | 
  <a href="https://www.softeng.ox.ac.uk/signin/" title="Sign in">Sign
  in</a>
</span>
-->

<div id="content">

<h1 style="vertical-align:middle"><img align="middle" valign="middle" style="vertical-align:middle" border="0" src="../images/MCH.jpg"> Advanced Concurrency Tools: Model Checking</h1>
      <div>
	
	<p>The rigorous development of a complex concurrent or distributed
system is an immense challenge for any organisation.  This course
teaches principles of structure and refinement that are particularly
useful in understanding such systems.  An essential feature of this
course is the comprehensive tool support that is provided for
reasoning about concurrent systems: communications protocols,
distributed databases, and control systems.</p>
<h4>Course dates</h4>
<center>
Future courses yet to be planned.<br>
</center>
<h4>Objectives</h4>
<p>Students will gain experience in applying the Communicating
Sequential Processes (CSP) formalism to realistic problems in
specification and design. They will also gain experience in using a
practical toolset for refinement testing and analysis.</p>
<h4>Contents</h4>
<p><dl> <dt><span>CSP:</span></dt> <dd> process syntax; events; abstraction; refinement.</dd> <dt><span>Observations:</span></dt> <dd> execution; history; testing; deadlock; livelock.</dd> <dt><span>Model-checking:</span></dt> <dd> tools; principles; context.</dd> <dt><span>Protocols:</span></dt> <dd>: modelling and analysis; errors; media specification.</dd> <dt><span>Control systems:</span></dt> <dd> interaction; failure; interference. </dd> <dt><span>Combinatorics:</span></dt> <dd> transition systems; modelling large systems. </dd> <dt><span>Time:</span></dt> <dd> timing constraints; timeouts; delays.</dd> <dt><span>Non-interference:</span></dt> <dd> security; safety; fault-tolerance.</dd> <dt><span>Dealing with state explosion:</span></dt> <dd> data-independence; compression strategies.</dd> </dl></p>
<h4>Requirements</h4>
<p><p>Students will be expected to have a working knowledge of the CSP notation: <a href="http://www.softeng.ox.ac.uk/subjects/CDS.html">Concurrency and distributed systems</a> would be an ideal preparation. Any student who has not taken <a href="http://www.softeng.ox.ac.uk/subjects/CDS.html">Concurrency and distributed systems</a> should ask for advice before registering for this course.</p></p>

	
      </div>

<br>

    
[an error occurred while processing this directive]

<!--  mainnav div starts -->
<div id="nav">     
 <h2 id="mainsections">Main sections</h2>
 
 <h2 id="inthissection">Programme</h2>
 <ul class="mainnav" >
  <li>
   <a href="../" title="Return to the Home page" class="menu" >Home</a>
  </li>
  <li>
   <a href="../programme/index.html" title="About the programme" class="menu">About</a>
  </li>
  <li>
   <a href="../programme/history.html" title="The history of the Programme"  class="menu">History</a>
  </li>
  <li>
   <a href="../programme/people.html" title="The people involved" class="menu">People</a>
  </li>
  <li>
   <a href="http://www.cs.ox.ac.uk" title="Department of Computer Science" class="menu">Department</a>
  </li>
  <li>
   <a href="../programme/contact.html" title="Getting in touch" class="menu">Contact us</a>
  </li>
  </ul>
  
  
  <h2 id="inthissection">Courses</h2>
  <ul class="mainnav">
  <li>
   <a href="../courses/" title="About the courses" class="menu">About</a>
  </li>
  <li>
   <a href="../courses/subjects.html" title="Subjects offered" class="currentsection">Subjects</a>
  </li>
  <li>
   <a href="../courses/calendar.html" title="Course dates" class="menu">Calendar</a>
  </li>
  <li>
   <a href="../courses/booking.html" title="How to book a place on a course" class="menu">Booking</a>
  </li>
  </ul>
  
  
  <h2 id="inthissection">Study</h2>
  <ul class="mainnav">
  <li>
   <a href="../study/" title="Flexible, postgraduate study" class="menu">About</a>
  </li>
  <li>
   <a href="../study/awards.html" title="Academic awards" class="menu">Awards</a>
  </li>
  <li>
   <a href="../study/fees.html" title="University fees" class="menu">Fees</a>
  </li>
  <li>
   <a href="../study/apply.html" title="How to apply" class="menu">Applications</a>
  </li>
  <li>
   <a href="../study/collegiate.html" title="Collegiate University" class="menu">Colleges</a>
  </li>
  </ul>
  
  
  <h2 id="inthissection">Resources</h2>
  <ul class="mainnav">
  <li>
   <a href="../handbook/" title="Handbook" class="menu">Handbook</a>
  </li>
  <li>
   <a href="../brochures/" title="Brochures" class="menu">Brochures</a>
  </li>
 </ul>



[an error occurred while processing this directive]