| HILT 2016 |
|
ACM SIGAda’s High Integrity Language Technology
International Workshop on
Model-Based Development and Contract-Based Programming
as part of Embedded Systems Week
(ESWEEK)
Software systems sense and affect real world objects and processes in order to realize important real-world systems. For these systems to function correctly, such software has to obey constraints inherited from the real world. As a result, the real-world semantics and hence the semantics of software are far more complex than most engineers realize.
Typically, neither important characteristics of real-world entities nor the relationships between such entities and their machine-world representations are specified explicitly in code, and important opportunities for detecting errors due to mismatches are lost.
In this presentation, I will discuss the interpretation of logic and introduce real-world types to document in software both relevant characteristics of real-world entities and the relationships between real-world entities and machine-level representations. These constructs support specification and automated static detection of mismatches in programs written in ordinary languages. I will present a prototype implementation of the approach for Java and case studies in which previously unrecognized real-world type errors in several real systems were detected.