Abstract-Business Process Modelling har fått ökad relevans inom mjukvaruutveckling. Tillgängliga noteringar, såsom BPMN, gör det möjligt att beskriva komplexa organisationers verksamhet. Å ena sidan minskar detta kommunikationsklyftan mellan domänexperter och IT-specialister. Å andra sidan gör detta det möjligt att klargöra egenskaperna hos de programvarusystem som införs för att ge automatiskt stöd till sådan verksamhet. Bristen på formella semantik hindrar dock den automatiska kontrollen av relevanta egenskaper. I detta dokument presenteras en ny verifieringsram för BPMN 2.0, kallad BProVe. Den bygger på en operationell semantik, som genomförs med hjälp av MAUDE, utformad för att göra verifieringen allmän och effektiv. En komplett verktygskedja, baserad på Eclipse modellering miljö, möjliggör rigorös modellering och analys av affärsprocesser. Metoden har validerats med hjälp av mer än tusen modeller som finns tillgängliga i ett allmänt tillgängligt arkiv. Förutom att visa prestandan hos BProVe, visar denna validering sina praktiska fördelar när det gäller att identifiera korrekthetsproblem i verkliga modeller.
Corradini m.fl. REF presenterar BProVe, ett verktyg för verifiering av affärsprocesser som modelleras i BPMN.
BProVe: A formal verification framework for business process models
{'venue': '2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)', 'journal': '2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)', 'mag_field_of_study': ['Computer Science']}