Invited Speakers
Rick Hull, IBM T. J. Watson Research Center, USA
Formal Study of Business Entities with Lifecycles: Use Cases, Abstract Models, and Results
Over the past several years there has been increasing interest in frameworks for workflow, web service composition, and Business Process Management (BPM) that incorporate "data" to be a first-class citizen along with "process". In the approach of Business Entities with Lifecycles (BEL), also known as "business artifacts", the basic building block for a business process includes both a data schema (perhaps based on attribute/value pairs or XML) and a lifecycle schema (perhaps based on finite state machines, Petri nets, or ECA rules). This and related models of data-centric BPM raise new challenges for the verification community because of the infinite state space. Nevertheless, the particular focus of BEL has enabled the development of some useful results and techniques for this context.
This talk will begin by motivating the BEL approach, illustrating different ways that business entities arise in practice, and identifying some representative verification and synthesis challenges. Next an abstract model, along with some variations, is described that captures the essential components of the practical BEL models. Finally, some representative analysis and synthesis results are surveyed, to illustrate the kinds of results and techniques that are emerging in this area.
Shriram Krishnamurthi, Brown University, USA
Policy Analysis with Margrave
Access-control policies control data dissemination in domains from health-care to social networks. Similar policies also govern various aspects of firewalls and routers.
The subtle nature of these policies suggests this is a natural domain to apply formal methods, while the separate authoring of policies in domain-specific languages affords opportunities for powerful analysis. It is, however, unclear that the straightforward application of verification is appropriate or useful. We will discuss these issues, as well as our concrete tools and results.
Joint work with Kathi Fisler, Dan Dougherty, Tim Nelson, Chris Barratt, Michael Tschantz, Leo Meyerovich.