CIS 771 Software Specifications

As the complexity of software increases, it is crucial that the software engineering community move toward automated tool-based solutions that provide deeper semantic reasoning about system specifications.

While courses that present best practices of software development based on existing commercial tools and development processes are valuable, we chose to focus this graduate course on software specification and verification technologies that provider deeper semantic reasoning and verification of development artifacts including functional models, architecture, and source-code implementations. Thus, the material in this course does not cover existing industry software development processes and tools. Rather, it presents cutting-edge tool-based specification and verification technologies that have the potential to be incorporated into industry tools and development workflows within the next 3-5 years.

The current version of this course presents three tools that embody the principles above for different stages of software development:

• Alloy - a text-based language for modeling the structure of primary system entities along with relationships and constraints between these entities. Alloy is accompanied by an automated analyzer that uses SAT-based technology to support reasoning about Alloy structures/constraints and semantic querying that provides example system instances that conform or violated stated constraints.

• USE - a tool for defining UML class diagrams with OCL constraints with an underlying reasoning engine that allows OCL constraints to be tested again specific system instances defined by developers.

• SPARK and Bakar Kiasan - SPARK is one of the premier commercial development frameworks for high-assurance software. The SPARK language is a subset of Ada designed for programming and verifying high assurance applications such as avionics applications certified to DO-178C Level A. It deliberately omits constructs that are difficult to reason about such as dynamically created data, pointers, and exceptions. SPARK includes a procedure annotation language for specifying pre/post-conditions and embedded assertions. Bakar Kiasan is a framework developed by the SAnToS research group at Kansas State for highly-automated checking of SPARK contracts.

For more information about getting started in this course, please see the Getting Started link the left tool bar. The pedagogical material for this course (include videos of lectures, slides, examples, etc.) can be found at the Lectures link.

If you are a faculty member from an another institution interested in using this course material, please contact Robby about obtaining a distribution bundle.