(joint work with Wolfgang Ahrendt and Frank de Boer)
We give a representation of a weakest precondition calculus for abstract object creation in dynamic logic, the logic underlying the KeY theorem prover. This representation allows to both specify and verify properties of objects at the abstraction level of the (object-oriented …
read moreIn this meeting we would like to discuss the development of the Mist programming language. Our goal is to create a new programming language with many promising features, prominently among them an integrated proof framework. The hope is to automatically generate formal proof of correctness, rather than relying solely on …
read moreThe complex interactions appearing in service-oriented computing make coordination a key concern in service-oriented systems. In this paper, we present a fault-based method to generate test cases for component connectors from specifications. For connectors, faults are caused by possible errors during the development process, such as wrongly used channels, missing …
read moreSoftware Tools Demonstration
A number of our colleague in SEN3 have been developing software tools in the context of their various projects. Many, but not all, of these tools are related to Reo and are integrated into the Eclipse Coordination Tools (ECT). The ECT also incorporates some tools developed by …
read moreThe two fields of automata theory and formal languages on the one hand, and concurrency theory on the other hand, have developed independently, but have a lot in common. The one is a basic model of computation that gives us notions like algorithm and computability, the other is a basic …
read moreFor polynomial functors G, we show how to generalize the classical notion of regular expression to G-coalgebras. We introduce a language of expressions for describing elements of the final G-coalgebra and, analogously to Kleeneâs theorem, we show the correspondence between expressions and finite G-coalgebras.
read moreIf, as a well-known aphorism states, modelling is for reasoning, this paper is an attempt to define and apply a formal semantics to UML sequence diagrams in order to enable rigourous reasoning about them. Actually, model transformation plays a fundamental role in the process of software development, in general, and …
read moreIn this talk I present some my recent work on service-oriented middleware for multi-network environments which is part of EU ICT PLASTIC project.
Modern mobile devices are featured by multiple network interfaces that allow them to communicate using not only cellular network infrastructures but also other independently administered networks. We …
read moreUnderstanding and implementing Reo has been challenging due to interaction of the 'channel metaphor', which is an inherently local notion, and the non-local nature of constraint propagation imposed by composition. In this work, the channel metaphor takes a back seat, and we focus on the behavioural constraints imposed by the …
read moreCurrently, there are no well-established techniques to ensure dynamic and ongoing compliance of services-oriented applications to business regulations that come out from legislative and regulatory documents such as Basel II1, IFRS2, MiFID3, LSF4, HIPAA, Tabaksblat5, and the Sarbanes-Oxley6 Act, as well as from internal movements of business stakeholders towards Quality …
read more