Modern computing systems are mobile, networked, and highly concurrent – characteristics that make them complex and risky to develop, especially when we trust such systems with our money, resources, businesses or lives. Building abstract models of computing systems makes it possible to design better systems. Such models provide a basis to reason about the correctness of designs and allow exploring alternatives.
The AMBER group’s work aims to help contain risk by equipping engineers with methods and tools that allow them to explore, verify and refine the properties of such complex systems by means of models with well-founded semantics. Such model-based engineering can permit detection of optimal (and defective!) designs long before the sometimes expensive commitment is made to implementations on real hardware.