Graphical models for business processes are very large and cumbersome to build. Reusable process patterns can make this modeling task much easier. While using reusable components is a well-explored subject in software engineering, not much has been done in the context of business process modeling. In this paper, we will present an extension to Business Process Model and Notation (BPMN), the standard notation for modeling business processes, in the form of reusable Process Patterns. We introduce a type system for these patterns and use it to define a valid embedding of a process pattern in a larger model. We also introduce the formal notations and show that business processes modeled using our extended notation can be translated to BPMN. We present a case study to demonstrate the applicability of the process pattern and further quantify its characteristics using a set of criteria. We also implement a modeling tool for users to model business process using process patterns.

We present the design of a multicore version of FreeRTOS, a popular open source real-time operating system for embedded applications. We generalize the scheduling policy of FreeRTOS to schedule the n highest-priority longest-waiting tasks, for an n-core processsor. We use a locking mechanism that provides maximum decoupling between tasks, while ensuring mutually exclusive access to kernel data-structures. We provide an implementation of the portable part of FreeRTOS (written in C) and provide the device specific implementation of the locking mechanism for Intel and ARM Cortex multicore processors. We model the locking mechanism and the locking protocol used by the API's in the Spin model-checking tool and verify that the design is free from dataraces and deadlocks. Finally, we extend the existing FreeRTOS Windows simulator to simulate our multicore version of FreeRTOS, and evaluate its performance on some demo applications.

In order to maximize cost and quality gains, industrial automation systems need to incorporate the best practices of software engineering in their application development process. However, this requires the right set of tools and methodologies that cater to the needs of the automation domain. While there have been a few efforts towards applying state-of-the-art software engineering tools and techniques to the automation domain, these have not been universally adopted. This paper discusses some of the challenges in adopting software engineering principles for industrial automation application development. Further, the paper presents a case for research activities to look for more practical solutions for industrial applications.

We introduce a visual notation for local specification of concurrent components based on message sequence charts (MSCs). Each component is a finite-state machine whose actions are MSCs that specify its local view of the overall communication in the system. These local MSCs are composed into coherent global scenarios using a separately specified set of transactions. Intuitively, each MSC represents a phase of interaction. We introduce a mechanism to overlap phases that allows complex interactions to be specified without obscuring the logical structure of the constituent scenarios. Our notation combines the global view available in models such as high-level message sequence charts (HMSCs) with the local, asynchronous structure captured by message-passing automata (MPA). In fact, both HMSCs and MPAs can be captured as special cases of our formalism. In this paper we focus on the syntax and formal semantics of our notation, with examples that illustrate why this approach is more natural for capturing real-life specifications. We also describe an approach to use automated tools to analyze systems specified using our notation.

Asynchronous systems programs are usually written in an event-driven style which is tailored for performance rather than analyzability. Such programs have non-sequential control ow and make heavy use of heap data structures to store and retrieve state related to pending operations. As a result, existing tools that analyze sequential programs are ine ective in analyzing asynchronous systems components. We describe clarity, a programming language that enables analyzable design of asynchronous components. clarity has three novel features: (1) Nonblocking function calls that allow event-driven code to be written in a sequential style. If a blocking statement is encountered during the execution of such a call, the call returns and the remainder of the operation is automatically queued for later execution. (2) Coords, a set of high-level coordination primitives, encapsulate common interactions between asynchronous components and make high-level coordination protocols explicit. (3) Linearity annotations delegate coord protocol obligations to exactly one thread at each asynchronous function call, transforming a concurrent analysis problem into a sequential one. We demonstrate how these language features enable both a more intuitive expression of program logic and more e ective program analysis most checking is done using simple sequential analysis. We describe our experience in developing, testing, and analyzing a network device driver using clarity. 1.