.. _chapter-overview:

Overview
--------

In this chapter, we provide an outline of the course, along with a brief motivation and key learning outcomes.


Motivation
^^^^^^^^^^

As embedded and distributed systems are becoming ever more ubiquitous,
we depend increasingly on the correctness of the software that
controls such systems.
This course studies the formal specification, verification, and
synthesis of software.


Key learning outcomes
^^^^^^^^^^^^^^^^^^^^^

- An understanding of the role of formal methods in the construction
  of software systems
- Proficiency in the representative methods and tools, such as

  - design-by-contract 
  - property-based testing
  - model-checking sequential and concurrent systems


Course outline
^^^^^^^^^^^^^^

To be expanded...

- software engineering context
- logic foundations
- design by contract
- property-based testing
- modeling and model checking
   - sequential systems 
   - concurrent systems 
- run-time verification


Bloom's taxonomy
^^^^^^^^^^^^^^^^

The letters refer to the successive levels of learning from the cognitive domain of `Bloom's taxonomy <http://en.wikipedia.org/wiki/Bloom's_taxonomy#Cognitive>`_:

- K: know/remember the term
- C: comprehend/understand the concept
- A: apply the technique
- analyze/evaluate/create (advanced levels)

.. todo:: map Bloom levels to course outline