A Workflow Methodology for Realising Concurrent and Verified Systems
Peter H. WELCH (a) and Jan Bækgaard PEDERSEN (b)
(a) School of Computing, University of Kent, UK
(b) Department of Computer Science, University of Nevada Las Vegas, USA

Abstract. Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum – no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as an advanced discipline for later study. Formal verification of system properties remains considered an advanced and difficult subject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. Our experience, from over 30 years of teaching concurrency and formal methods, is that when both are presented together, there is a happy symbiosis providing strong mutual support that transforms both disciplines from advanced and hard to basic and simple. Of course, the model of concurrency and formal methods presented must be simple, powerful and consistent with each other ... and, of course, we are talking about process orientation and process algebra.

As with many other disciplines, it is important to use a well-defined methodology that shows how aspects of the disciplines relate to each other and how work flows between them. We introduce a workflow methodology for the mutual development and verification of concurrent systems that serves as a good foundation for students and novices – as well as mature software engineers – learning to integrate formal verification into their development cycle. Such a workflow methodology should be a fundamental element of any future software engineer's tool kit – to be used, together with established software engineering techniques, every day as a matter of course. Concurrency and verification can and should live in symbiosis. By following a well-defined workflow that makes this explicit, major benefits (such as faster development, right-first-time and easier maintenance) can be realised.

This talk will present an approach developed over many years at Kent and UNLV for teaching concurrency with verification and share some of our materials and experiences.

Brief Background

Peter Welch is Emeritus Professor of Parallel Computing at the University of Kent. He graduated in Mathematics from Warwick University (England) in 1969, taking his PhD in Computer Science from the same institution in 1975. His doctoral research was on semantic models for the lambda-calculus.

For the past 35 years, his main area of research and teaching has been in the field of concurrency and parallel computing. Applications of theory include a CSP model of Java thread synchronisation (that enables formal verification of Java multithreaded code) and CSP-based design rules for process network hierarchies (with proven safety properties such as the absence of deadlock, livelock and starvation). Long term research includes the design and development of tools supporting those rules, the design and compilation of parallel languages (occam-pi, ...), very lightweight CSP kernels (including efficient targeting of multicore) and the CSP class libraries for Java (JCSP).

He was Principal Investigator for the Kent part of the CoSMoS project (2007-2012), a joint project with the University of York. CoSMoS researched patterns and frameworks for complex systems modelling and simulation, including the controlled engineering of emergent behaviours. Typical models run to tens of millions of concurrent processes, with ever changing network sizes and topologies. Large models (needed for rich and interesting behaviours to emerge) rely on the lightweight concurrency support of occam-pi (for execution) and the CSP and pi-calculus process algebras (for formal, and informal, reasoning).

He is Emeritus Member member of the IFIP Working Group 2.4 on Software Implementation Technology. WG2.4 consists of engineers from industry and academia from all round the world and meets every nine months or so for a week in interesting locations. IFIP is the International Federation for Information Processing, founded in 1959 and is the unbrella organisation for most learned societies in Computer Science (including the ACM and IEEE in the USA and the BCS in the UK).

Distributing CSP Process Networks over MPI Clusters
Gabriella AZZOPARDI, Kevin VELLA and Adrian MUSCAT, Department of Computer Science, University of Malta, Msida, Malta

Abstract. This work investigates a range of algorithms and techniques for automatically distributing CSP process networks over an MPI cluster. A CSP library was developed to provide the necessary functionality for implementing CSP-based concurrent applications on top of MPI. The library enables seamless communication between processes on the same node and processes across different nodes. A new configuration language was implemented to provide a straightforward way to map processes onto cluster nodes. This was designed in such a way to allow for mapping the same application using different mapping algorithms without having to recompile the application. The resulting proof-of-concept system was then used to evaluate the suitability of well-known graph partitioning algorithms for distributing a suite of CSP-based applications across a compute cluster, with the aim of reducing application execution time in each case. The experimental results are presented in summary form and briefly analysed.

Event-driven, Collaborative and Adaptive Scientific Workflows on the Grid
Jonas BARDINO, Martin REHR and Brian VINTER, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. Exponential growth in scientific data set sizes and corresponding computation needs, forces scientists and engineers to structure and automate experiments in workflows running on distributed architectures. In eScience the flows typically evolve gradually from intensive experimentation and often involve multiple participants from separate organisations. Thus, there’s a need for infrastructures supporting such highly dynamic and collaborative workflows. Despite much attention to scientific workflows in recent years, most existing systems tend to be single-user top-down approaches, which are inherently best suited for static and fixed flows with all steps known up front. In this work we introduce a simple general rule-based model for event-driven work-flows based on data change triggers. A bottom-up workflow approach, that enables a high level of automation and allows dynamically changing flows – with or without manual user interaction. It is realised with an implementation on top of the Minimum intrusion Grid (MiG), which helps de-couple workflow design from underlying execution concerns, and provides built-in collaboration and sharing across organisation boundaries. However, the model itself applies to much wider range of scenarios, and other such possible implementation methods are briefly outlined.

Asynchronous Readers and Asynchronous Writers
Antoon H. BOODE and Jan F. BROENINK, Robotics and Mechatronics, CTIT Institute, University of Twente, the Netherlands

Abstract. Reading and writing is modelled in CSP using actions containing the symbols ? and !. These reading actions and writing actions are synchronous, and there is a one-to-one relationship between occurrences of pairs of these actions. In CPA 2016 we introduced the half-synchronous alphabetised parallel operator, X⇓Y, which disconnects the writing to and reading from a channel in time. We introduce in this paper an extension of X⇓Y, where the definition of X⇓Y is relaxed: the reading processes are divided into sets which are set-wise asynchronous, but intra-set-wise synchronous, giving full flexibility to the asynchronous writes and reads. Furthermore we allow multiple writers to the same channel and we study the impact on a Vertex Removing Synchronised Product. Advantages are that the extension of X⇓Y gives more flexibility by indexing the reading actions and allowing multiple write actions to the same channel. Furthermore the extension of X⇓Y reduces the end-to-end processing time of the processor or coprocessor in a distributed computing system. We show the effects of these advantages in a case study describing a Controlled Emergency Stop for a processor-coprocessor combination.

Building a C++CSP Channel Using C++ Atomics: a Busy Channel Performance Analysis
Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK

Abstract. Mutex-based implementations of synchronous channels are slow. This work investigates atomic operations as a technique to improve communication efficiency between two threads via a busy channel. Such a channel provides faster communication than a mutex-based one where the number of threads is identical to the hardware concurrency. To evaluate communication performance, a communication time benchmark is used alongside a selection time benchmark. The communication time benchmark is scaled to evaluate the impact of thread counts greater than the available hardware. Results show that an above ten-times improvement in communication time is possible when the hardware supports the threads fully. The improvement drops as further threads are added to the system due to operating system scheduling taking over the determination of thread activeness. Selection time similarly shows improvement when thread count matches hardware, but likewise reduces as thread count increases. We can conclude that a busy channel is useful in an environment where the thread count matches the available hardware, which is of interest to parallel application developers or control systems with similar properties.

What are Communicating Process Architectures? Towards a Framework for Evaluating Message-passing Concurrency Languages
Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK

Abstract. What does it mean to be a message-passing concurrent language? This work attempts to build a framework for classifying such languages by judging four in regards to features and performance. Features of process calculi are used to evaluate Go, Rust, Erlang, and occam-pi. Furthermore, standard communication time, selection time, and multicore utilisation are examined. Although each of these languages use message-passing concurrency, their approaches and characteristics are different. We can start to build an initial classification based on message-passing type, language support, and feature support. Such classification allows an initial discussion of the suitability of a the evaluation framework, whether it is useful, and how it can be expanded. Approximately 100 further languages have been identified as potentially supporting message-passing concurrency to further build up the classification.

Concurrent Composition of I/O Redundancy Behaviors in Go
Klaus Birkelund JENSEN and Brian VINTER, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. The Go programming language defines simple I/O interfaces that any type may implement. In this paper we introduce a Go package that allows arbitrary implementations of these interfaces to be composed into RAID-like redundant (and/or) high-performance striped arrays. The package also allows spares to be added for fail-over functionality. The package is focused on providing a highly available write setting that tolerates multiple failures but can always receive data as long as a single redundant path exists. This is achieved by allowing reads to be unavailable in the presence of failures. The package is highly concurrent and parallelised and exploits the Go programming language’s built-in light-weight concurrency features.

Implementing a MIPS processor using SME
Carl-Johannes JOHNSEN, Department of Computer Science, University of Copenhagen, Denmark

Abstract. The Synchronous Message Exchange (SME) model, is a programming model, which closely resembles the CSP model and which is suitable for describing hardware. This paper aims to combine the theory taught in a machine architecture class with the SME model, by implementing a MIPS processor using SME. The paper shows how to construct the components of a MIPS processor as SME processes and how to connect them by using SME busses. Furthermore, extensions to the processor are demonstrated through the introduction of additional instructions and pipelining the processor.

Automatic Code-generation for Library Method Inclusion in Domain Specific Languages
Mads Ohm LARSEN, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. Performance is important when creating large experiments or simulations, however it would be preferable not to lose programmer productivity. A lot of effort have already been put into creating fast libraries, for example for linear algebra based computations (BLAS and LAPACK). In this paper, we show that utilizing these libraries in a DSL made for productivity will solve both problems. This is done via automatic code-generation and can be extended to other languages, libraries, and features.

Co-simulation Design towards Cyber-Physical Robotic Applications -- Leveraging FMI Standard and CSP Semantics
Zhou LU and Jan F. BROENINK, Robotics and Mechatronics, CTIT Institute, University of Twente, the Netherlands

Abstract. Designing a software controller for multi-task automated service robotics is becoming increasingly complex. The combination of discrete (cyber) and continuous (physical) domains and multiple engineering fields makes it quite challenging to couple different subsystems as a whole for further verification and validation. Co-simulation is widely used to evaluate connected subsystems in the very early design phase and in an iterative development manner.

Leveraging on our previous efforts for a Model-Driven Development and simulation approach, that mainly focused on the software architecture, we propose a co-simulation approach adopting the Functional Mock-up Interface (FMI) standard to co-simulate the software controller with modelled physical plant dynamics. A model coupling approach is defined that involves the model transformation from a physical plant model implementing the FMI interface (denoted as Functional Mock-up Unit, FMU) to a Communicating Sequential Processes (CSP) model. The Master Algorithm is (semi-)automatically generated from a co-simulation model that is formalised with CSP syntax to orchestrate the communication between different FMUs. Additionally, an optimized algorithm with roll-back mechanism is defined to eliminate the delay existing in a feedback loop. Finally, an example is used to illustrate the co-simulation approach, verify its working (at least, for this example) and to analyse the roll-back algorithm.

Formal Analysis of Video Encoding Application within Map/Reduce
M. Carmen RUIZ (a), Diego Pérez LEÁNDREZ (a) and Damas GRUSKA (b)
(a) Universidad de Castilla-La Mancha, Spain
(b) Comenius University, Slovakia

Abstract. Cloud computing is the infrastructure of choice for compute and data intensive systems providing flexible number of resources for software applications: that is, the processing capacity assigned to an application can be adapted to its needs. Nevertheless, in a cloud pay–per–use model, the number of demanded resources must be taken into account in order to minimise the costs. Our main goal is to reason about a cloud-aware application’s resource usage by means of the Timed Process Algebra BTC and study the trade–offs between an application’s response time and resource usage. On the other hand, video encoders are software applications that need a lot of resources and work on files of considerable size, therefore it seems reasonable to try to take advantage of the capacity offered by cloud computing to accelerate the coding process. The H.264 standard is the most widely–scrambled encoding solution, although other standards are being developed and tested to be the latter’s successors, such as H.265 or HEVC. In this paper, the video encoder H.265 will be adapted following the MAP/REDUCE paradigm in order to be able to be executed in Hadoop. Then, its algebraic formalization will be developed by BTC and validated on a real private cloud environment. Finally, we will carry out a performance evaluation using the BAL tool.

Big Data Analysis with Skeletons on SOFA
Kenneth SKOVHEDE and Brian VINTER, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. This paper explores how a skeleton-based approach can be used to perform big data analysis. Running on top of a distributed storage system, we add a stream-oriented skeleton-based query system and show how to run a number of classic Big-Data benchmarks.

A Concurrent Data Collection Environment for WAsteful COMmunication SAtellite System
Tor SKOVSGAARD (a), Patrick Dyhrberg SØERENSEN (a), Lawrence J. DICKSON (b), Lindsay O'Brien QUARRIE (b) and Brian VINTER (c)
(a) Department of Computer Science, University of Copenhagen, Denmark
(b) Space Sciences Corporation, Lemitar, New Mexico, USA
(c) Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. WACOMSAS (WAsteful COMmunication SAtellite System) uses the Transterpreter to demonstrate a finite, static occam-Pi design for a ground station that communicates with at most four passing satellites at a time. There are an indefinite number of satellites, each of which may never return. The satellites are not coded in occam-Pi, and external channels with mobile channel-ends are used to communicate with them according to a switchboard analogy applicable both to hardware and software interfaces.

Concurrency Issues in Ordinary Place Transition Petri Nets
Anthony Spiteri STAINES, Department of Computer Information Systems, University of Malta, Malta

Abstract. This paper briefly explains some basic concurrency issues that are present when modeling with classical place transition nets. Many users assume that certain Petri net structures are concurrent or concurrency free. However, it can be shown that concurrency does not depend only on the structure but also on the distribution of resources in the net. Some toy examples are given to show the different possibilities and concurrency is classified into (i) dependent and (ii) temporal (weak) concurrency. Some findings are presented.

Teaching Concurrency: 10 Years of Programming Projects at UCPH
Brian VINTER and Mads Ohm LARSEN, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. While CSP is traditionally taught as an algebra, with a focus on definitions and proofs, it may also be presented as a style of programming: process oriented programming. For the last decade UCPH has been teaching CSP as a mix of the two, including both the formal aspects and process oriented programming. The present paper summarises the work that has been made to make process oriented programming relevant to students, through programming assignments where process orientation is clearly simpler than an equivalent solution in imperative programming style.

Unifying Concurrent Programming and Formal Verification within One Language
Peter H. WELCH (a), Jan Bækgaard PEDERSEN (b), Frederick R.M. BARNES (a), Carl G. RITSON (a) and Neil C.C. BROWN (c)
(a) School of Computing, University of Kent, UK
(b) Department of Computer Science, University of Nevada Las Vegas, USA
(c) Department of Informatics, King's College London, UK

Abstract. This is a proposal for the formal verification of occam-pi programs to be managed entirely within occam-pi. The language is extended with qualifiers on types and processes (to indicate relevance for verification and/or execution) and assertions about refinement (including deadlock, livelock and determinism). The compiler abstracts a set of CSP_M equations and assertions, delegates their analysis to the FDR model checker and reports back in terms related to the occam-pi source. The rules for mapping the extended occam-pi to CSP_M are given. The full range of CSP_M assertions is accessible, with no knowledge of CSP formalism required by the occam-pi programmer. Programs are proved just by writing and compiling programs. A case study analysing a new (and elegant) solution to the Dining Philosophers problem is presented. Deadlock-freedom for colleges with any number of philosphers is established by verifying an induction argument (the base and induction steps). Finally, following guidelines laid down by Roscoe, the careful use of model compression is demonstrated to verify directly the deadlock-freedom of an occam-pi college with 10²⁰⁰⁰ philosphers (in around 30 seconds). All we need is a universe large enough to contain the computer in which the college and its philosophers can live.

DOMASCOS – DOMAin Specific COncurrency Skeletons
Brian VINTER (a), Kevin CHALMERS (b), Kevin VELLA (c), John Markus BJØRNDALEN (d) and Jan F. BROENINK (e)
(a) Niels Bohr Institute, University of Copenhagen, Denmark
(b) School of Computing, Edinburgh Napier University, UK
(c) Department of Computer Science, University of Malta, Msida, Malta
(d) Department of Computer Science, University of Tromsø, Norway
(e) Robotics and Mechatronics, CTIT Institute, University of Twente, the Netherlands

Existing approaches to concurrent programming, albeit essential, are easily used incorrectly. Testing is difficult due to the inherent non-determinism introduced by concurrency, especially in embedded systems (e.g., the Mars Rover catastrophe). DOMASCOS' goal is to produce (a) experts in concurrency programming and (b) libraries of concurrency program skeletons freeing applications from concurrency bugs – or, at least, significantly reducing their occurrence. Hence, programmers will no longer be required to implement their own concurrency mechanisms, but inherit guaranteed correct concurrency schemas directly from the DOMASCOS library. DOMASCOS addresses the problem of Reusable Concurrency for Modern System Design, supporting Europe to be at the forefront as the number of computationally enabled devices increases. DOMASCOS consists of concurrency groups of people sharing expertise in formally expressing correct concurrency, but differ in application domains: namely high-performance computing, GPU programming, embedded systems and robotics. The variety in applications ensures versatility of the skeletons and the shared concurrency knowledge ensures coherence in the team.

The application topics of DOMASCOS range from high performance computing, embedded systems, the creative industries, and robotics. These are all cross-sectional areas, key for the development for future innovation. Areas on which DOMASCOS will have an impact directly will be finance, big data, Internet of Things, games, autonomous systems, and working in extreme environments.

Building a Hand-held Cluster for £120
Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK

Abstract. Cluster computers are seen as expensive, space consuming, high energy platforms hidden away in universities and tech companies. Having your own cluster computer to explore parallelism ideas was not realistic for the majority of people. With the release of the Raspberry Pi things changed, and now it is possible to build a five node machine powered by USB that you can hold in your hand for as little as £120. This talk will describe how such a machine can be built with very little technical knowledge, and then provide an example of setting up MPI on the machine to allow simple distributed parallel applications to be explored. The system is not fast, and communicates via a shared USB 2.0 connection, but the principles of distributed parallelism can be explored. An example system will be available for demonstration purposes.

Working Concurrently: Applying Ideas from Concurrency to a Working Life.
Kevin CHALMERS, School of Computing, Edinburgh Napier University, UK

Abstract. Everyone is busy. No matter how much work you do, there always seems like there is more to do. Sometimes, we even seem to do nothing, spinning while we wait for someone else, or simply making no progress on our tasks. This presentation will show how we can take inspiration from computer science in general, and concurrency specifically, to help us organise our work. Concepts such as scheduling, context-switching, prioritisation, dependencies, logging, and time-slicing shall all be examined through the lens of personal effectiveness. The talk is a light-hearted one meant to inspire people into analysing their work practices, and is inspired by the book "Algorithms to Live By: The Computer Science of Human Decisions" by Brian Christian, but with a particular take from concurrency concepts applied more directly.

Rigorous Timing, Static OCCAM, and Classic CSP: Formal Verification for the Internet of Things
Lawrence J. DICKSON (a) and Jeremy M.R. MARTIN (b)
(a) Space Sciences Corporation, Lemitar, New Mexico, USA
(b) ITG Application Group, Lloyd's, London, UK

Abstract. Classic CSP is a "model without time" and yet contains time sequence and even a "time-out" or "sliding choice" operator (Roscoe, The Theory and Practice of Concurrency, 2005, p 80). The static occam language and the Transputer processor, both based on finite CSP, have time and other structure that make them a deliberate refinement of classic CSP; but occam is imperative and capable of doing completely general computing tasks. Programs written in occam and run on the Transputer can be proven correct and their behavior characterized down to cycle count. Classic CSP process descriptions of these same programs can also be investigated and proven using CSP techniques, including hiding.

This Fringe presentation, the first of a pair, will introduce these two approaches, using calculated assembly-code response of two-priority T2, T4, or T8 Transputers. We will begin with the n-process raw FIFO and the two-process store/shelf FIFO detailed in author Dickson’s book Crawl-Space Computing (pp. 111-120), using variable timing patterns for external communication. The true timing will be used to make sense of the abstract model of CSP in the real world, with and without hiding of internal channels.

The purpose of the investigation is to illuminate how rigorous conclusions can be drawn with a combination of CSP, occam-to-occam mappings, timing and sequence requirements. As time permits, we will expand the conclusions reached to IoT designs capable of serving multiple external communications and doing content calculations, treated as low-priority, time-consuming and nondeterministic.

Rigorous Timing, Static OCCAM, and Classic CSP: Mathematical Ground Truth
Lawrence J. DICKSON (a) and Jeremy M.R. MARTIN (b)
(a) Space Sciences Corporation, Lemitar, New Mexico, USA
(b) ITG Application Group, Lloyd's, London, UK

Abstract.  This Fringe presentation will continue the comparison of the two approaches from our first talk in rigorous mathematical detail. We introduce the mathematical concept of a Covering-with-Boundary (CwB), prove the equivalence of cycle-counted occam on a Transputer with this path diagram, and proceed to prove cases that avoid both divergence and effective divergence by finite restrictions. Due to static characteristics of occam-and-Transputer-based “Ground Truth,” we are also able to prove Hardware- Software Equivalence, and reach IoT conclusions that extend to non-digital payloads.

Pong Inspired Game Written in SME, Running on an FPGA
Carl-Johannes JOHNSEN, Department of Computer Science, University of Copenhagen, Denmark

Abstract. Given the prior knowledge of implementing SME (Synchronous Message Exchange) onto hardware, describing small hardware becomes very simple. This is shown by constructing a Pong inspired game in SME, in approximately a week, which runs on an FPGA (Field-Programmable Gate Array). The game uses the VGA port as output and the buttons on the board as input, and as such runs purely on the FPGA. The game consists of two larger parts: the VGA controller and the game logic, with the VGA controller being the most problematic part to implement.

T42 – Transputer Design in FPGA (Year Three Design Status Report)
Uwe MIELKE (a), Martin ZABEL (b) and Michael BRUESTLE (c)
(a) Infineon Technologies, Dresden, Germany
(b) Institut für Technische Informatik, Technische Universität Dresden, Germany
(c) Electronics Engineer, Vienna, Austria

Abstract. Our IMS-T425 compatible Transputer design in FPGA has so far taken over 300 design days. Up to last year, minimal effort was spent for verification. Now a regression test bench has been brought in place, which is targeted to verify the design conformance after any changes. This T42 Transputer Verification Suite is based on a TVS-1 work from Michael Bruestle, and compares the register output of 54 selected instructions versus a true T425 golden reference for up to thousands of data samples. It has already helped in T42 micro-code debugging and hardware refinement.

Concurrency, Intuition and Formal Verification: Yes, We Can! (Ben-Ari's Twin-Process Conundrum)
Jan Bækgaard PEDERSEN (a) and Peter H. WELCH (b)
(a) Department of Computer Science, University of Nevada Las Vegas, USA
(b) School of Computing, University of Kent, UK

Abstract. Not only can (and should) concurrency be introduced early in the undergraduate CS curriculum – but mechanisms for its formal analysis and verification can be presented that are intuitive, effective and easy to learn and apply. Further, this can be done without requiring students to be trained in the underlying formal mathematics. Instead, we stand on the shoulders of giants who have engineered the necessary mathematics into the concurrency models we use (CSP, π-calculus), the programming languages/libraries (occam-π, JCSP, Process-J) that let us design and build efficient executable systems within these models, and the model checker (FDR3) that lets us explore and verify those systems. All we require from our students are a love of the subject, a flair for programming and some time and effort. This talk presents some experience over the past ten years that lets us make these claims.

The reason for the "should" in the first sentence of this abstract is as follows. Multi-core architectures are now standard, with the number of cores per processor growing each year. Multi-processor networks are inescapable for super-computing problems and many (most?) forms of embedded computer platform. Engineers (and students) cannot avoid concurrent reasoning when dealing with these devices – avoidance leads to many bad things. Verification of this concurrent reasoning is mostly set aside (as it has generally been for sequential reasoning, we admit). A significant amount of professional development time and money is spent instead on testing software. However, testing and debugging concurrent programs is even more difficult than testing and debugging sequential programs: common faults are intermittent and not reproducible on demand. If the concurrency pattern is beyond the embarrassingly parallel (i.e., the processes need to engage with each other) and we have made some mistakes in design or coding, testing may never see these faults ... and our system will eventually fail in service (on Mars, for instance). So, we need to verify. Now, just as we need tools (e.g. programming languages) to produce executable systems, we need tools (e.g. model checkers) to produce verified systems. Language and model checker pairs need to live to the same concurrency model.

We present ``Ben-Ari's Conundrum'' as an example of how to follow the workflow and demonstrate its usability and wins. We invite the audience to have a go at predicting the solution to the conundrum in advance. The problem is something that may seem relatively straightforward, but turns out to not be quite as simple as it looks. Significant aspects of behaviour were overlooked by Ben-Ari for several years, until one of his students observed something that should not have happened.

VCSP - Towards a Process Oriented Scratch-Model?
Brian VINTER, Niels Bohr Institute, University of Copenhagen, Denmark

Abstract. Anyone who knows process oriented programming immediately acknowledges the claim that process orientation is well suited for games programming. As it turns out, this is easier acknowledged than done since there are no game programming frameworks that support an external threading library, but rather all insist on managing threads within the game framework. This fringe introduces an idea, as of yet without any implementation, to integrate visual effects directly within PyCSP.