Formal Language for Objects’ Transactions (ObTFL)

The disparity between software design and implementation, especially concerning IoT security and forensics, often lacks clarity and precision. Formal languages, rooted in mathematical rules, logic, and symbols, have proven priceless for expressing specifications and verifying system designs. Various semi-formal and formal languages, such as JSON, XML, predicate logic, and regular expressions, along with formal models like Turing machines, cater to specific domains. This paper introduces a novel formal language, named ObTFL (Object Transaction Formal Language), initially developed for IoT forensics and authentication purposes but later extended to encompass general distributed systems. The paper elucidates the syntax and semantics of ObTFL and presents several case studies showcasing its versatility and effectiveness.