Formal language for objects’ transactions

The gap between software design and implementation often results in a lack of clarity and precision. Formal languages, based on mathematical rules, logic, and symbols, are invaluable for specifying 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, serve specific domains. This paper introduces a new specification formal language, ObTFL (Object Transaction Formal Language), developed for general-purpose distributed systems, such as specifying the interactions between servers and IoT devices and their security protocols. The paper details the syntax and semantics of ObTFL and presents three real case studies—federated learning, blockchain for crypto and bitcoin networks, and the industrial PCB board with machine synchronization—to demonstrate its versatility and effectiveness in formally specifying the interactions and behaviors of distributed systems.