In this talk I discuss a mechanism for object creation which allows for an optimal use of bounds on the visible heap in model-checking of object-oriented programs.
read moreSimulation, testing and implementation of Reo
Service-based systems are software systems composed of autonomous components or services provided by different vendors, deployed on remote machines and accessible through the web. One of the challenges of software engineering is to ensure that such a system behaves as intended by its designer. The Reo coordination language is an …
read moreReo: Applications in Formalizing Standard Models
This presentation highlights applications of Reo in formalizing business models. We show how to apply Reo in formalizing modeling standards: BPMN, BPEL, UML Sequence Diagram and Activity Diagrams to provide means to model check such early products of software development. These transformations mainly are realized in Atlas Transformation Language, a …
read moreReo: Extended Semantics and Tools
In this second talk about Reo, I will briefly introduce several other semantic models that capture context-dependency in Reo connectors, namely, Intentional Automata and Reo Automata. Then I will introduce Action Constraint Automata which generalize Constraint Automata by allowing more observations on Reo ports. This model is used for describing …
read moreReo: Basics and Semantics
Over the past decades, coordination languages have emerged for the specification and implementation of interaction protocols for communicating software entities. This class of languages includes Reo, a platform for compositional construction of connectors. This talk comprises an introduction to Reo. It starts with an example that motivates the use of …
read moreOn the axiomatization of (weighted) language equivalence
In this talk I will present how we derived a sound and complete axiomatization of language equivalence for non-deterministic and weighted automata from a calculus of regular expressions for (weighted) bisimulation.
read moreAn Introduction to K Framework by Examples
K project was started in 2003 by Grigore Rosu, University of Illinois at Urbana Champaign (UIUC), for teaching puposes. Starting with 2010, K became a joint work between Formal Systems Laboratory (FSL) from UIUC and Formal Methods in Software Engineering (FMSE) groupfrom Al. I. University of Iasi (UAIC).
In the …
read moreAn Introduction to Coalgebra and Coinduction, using Regular and Context-free Languages
We give a summary of some of the existing work on coalgebra and coinduction: a general introduction to the coalgebraic framework is given, focussing especially on the instance of coalgebraic representations of regular and context-free languages, and deterministic automata. We show how Brzozowski derivatives of regular expressions fit into the …
read moreSpecifying Interfaces in Java in terms of Communication Histories using Attribute Grammars - part 2
We propose a new formal modeling language for the specification of interfaces in Java in terms of communication histories, i.e., sequences of messages. We show how attribute grammars provide a powerful separation of concerns between high-level protocol-oriented properties, which focus on the kind of messages sent and received, and …
read moreMulticore Programming in Object-Oriented Languages
We studied different languages and libraries that brought multicore programming methods into object-oriented languages. The methods included Actor model, software transactional memory, and data flow programming. The languages included Java, C++, Python, and C#.
read more