Formal Specification of the Internet of Things

State machines, originally named 'evolving algebras'[1,2] emerged as a model of computation that built on the concepts embodied in algebraic specifications. Amongst the many applications of abstract state machines, the formal definition of SDL [3], the ITU standard specification and description language [4], is one of the most striking. SDL has a graphical and textual language, a well-established record in telecommunications and embedded systems, and a history of revision and adaptation to meet changing real-world requirements.
This paper introduces SDL, briefly reviewing its background, formal definition, tool support and applications. It outlines the mechanisms by which SDL evolves to meet changing requirements, and discusses how SDL is currently being updated to meet the characteristic challenges posed by the Internet of Things (IoT) [5]. These include communicating devices with different characteristics operating in different physical environments, data of varying and uncertain quality, a wide variety of data analysis applications, and exposure to external systems at every level.
Examples are used to explore how SDL addresses these challenges, and how the language is likely to evolve in the future. The role of abstract state machines (ASMs) in specification, automated testing, application generation and deployment is outlined, and future directions for ASMs are identified.