The Invoicing Case Study in (E-)LOTOS

The informal requirements for the invoicing case study are analysed and interpreted. This leads to a high-level specification architecture that can be formalised. Specifications are presented in LOTOS (Language Of Temporal Ordering Specification). For comparison, specifications are also presented E-LOTOS (Enhancements to LOTOS) – the new version of LOTOS currently being standardised. Since LOTOS allows a balance to be struck between process-oriented and data-oriented modelling, specifications in both styles are given. The resulting specifications are evaluated in the context of LOTOS and formal approaches more generally