Eduard Babkin - PhD in Computer Science, Professor, Department of Information Systems and Technologies, Faculty of Business Informatics and Applied Mathematics, National Research University Higher School of Economics
Address: 25/12, Bolshaya Pecherskaya str., Nizhniy Novgorod, 603155, Russian Federation  
E-mail: eababkin@hse.ru

Anna Buzueva - Student, Department of Information Systems and Technologies, Faculty of Business Informatics and Applied Mathematics, National Research University Higher School of Economics
Address: 25/12, Bolshaya Pecherskaya str., Nizhniy Novgorod, 603155, Russian Federation  
E-mail: anna.a.buzueva@gmail.com

Kira Logvinova - PhD in Mathematics, Professor, Department of Information Systems and Technologies, Faculty of Business Informatics and Applied Mathematics, National Research University Higher School of Economics
Address: 25/12, Bolshaya Pecherskaya str., Nizhniy Novgorod, 603155, Russian Federation  
E-mail: klogvinova@hse.ru

      The article considers a problem of controversy analysis in business processes, and offers a solution of this problem proving the readers with the illustration based on the analyzing of complex healthcare business processes by the formal approach of relational logic. The approach suggested should facilitate efficiency of management in municipal healthcare organizations, specifically focusing on the aspect of quality improvement of integrated healthcare services for elder people.  The scientific method of analysis is based on the particular formalism of relational logic which is implemented in the language of a widely used logical tool - MIT Alloy Analyzer.  For business-process modeling we use   a prospective approach of enterprise ontology and particular modeling methodology DEMO (Design & Engineering Methodology for Organizations). That methodology allows for complete and unbiased description of the constructional model of modern enterprises. Analysis of DEMO models provides for detailed understanding of management processes and plays the foundational role in business reengineering and the developing of business-aligned ICT-infrastructure. An important part of our research includes developing the formal specifications of created business-process models which are suitable for application of formal verification methods. Aimed at the improving reusability of the developed methods of translation from DEMO models to the language of MIT Alloy Analyzer, a new meta-model of DEMO transactions was created.   Given the meta-model developed and real-life business processes of municipal healthcare enterprise we have built formal models of business-processes and have carried out their analysis of logical consistency including the temporal aspect.