Camilo Rueda

Mauricio Toro, Camilo Rueda, Carlos Agón et al.

Writing multimedia interaction systems is not easy. Their concurrent processes usually access shared resources in a non-deterministic order, often leading to unpredictable behavior. Using Pure Data (Pd) and Max/MSP is possible to program concurrency, however, it is difficult to synchronize processes based on multiple criteria. Process calculi such as the Non-deterministic Timed Concurrent Constraint (ntcc) calculus, overcome that problem by representing multiple criteria as constraints. We propose using our framework Ntccrt to manage concurrency in Pd and Max. Ntccrt is a real-time capable inter- preter for ntcc. Using Ntccrt externals (binary plugins) in Pd we ran models for machine improvisation and signal processing.

Mauricio Toro, Camilo Rueda, Carlos Agón et al.

In this paper we present Gelisp, a new library to represent musical Constraint Satisfaction Problems and search strategies intuitively. Gelisp has two interfaces, a command-line one for Common Lisp and a graphical one for OpenMusic. Using Gelisp, we solved a problem of automatic music generation proposed by composer Michael Jarrell and we found solutions for the All-interval series.

Néstor Cataño, Camilo Rueda, Tim Wahls

We present a machine-checked soundness proof of a translation of Event-B to the Java Modeling Language (JML). The translation is based on an operator EventB2Jml that maps Evnet-B events to JML method specifications, and deterministic and non-deterministic assignments to JML method post-conditions. This translation has previously been implemented as the EventB2Jml tool. We adopted a taking our own medicine approach in the formalisation of our proof so that Event-B as well as JML are formalised in Event-B and the proof is discharged with the Rodin platform. Hence, for any Event-B substitution (whether an event or an assignment) and for the JML method specification obtained by applying EventB2Jml to the substitution, we prove that the semantics of the JML method specification is simulated by the semantics of the substitution. Therefore, the JML specification obtained as translation from the Event-B substitution is a refinement of the substitution. Our proof includes invariants and the standard Event-B initialising event, but it does not include full machines or Event-B contexts. We assume that the semantics of JML and Event-B operate both on the same initial and final states, and we justify our assumption.