This paper presents a new approach and design model targeting hybrid designer- and operator-defined performance budgets for timing and energy consumption. The approach is based on Petri Nets formalism. As the cognitive load is typically high while using formal methods, this increases the chances of mistakes. Our approach is focused on the readability aspects and aims to decrease the cognitive load of developers. We illustrate the proposed approach on example of a sample embedded multi-media system, a modern digital camera.

In this paper we present a formal framework for analysis and optimisation of the requirements specifications of systems developed to apply in several countries. As different countries typically have different regulations/laws as well as different cultural restrictions, the corresponding specific requirements might differ in each particular case. Our framework provides a basis for (1) systematic and formal analysis of the diversity and interdependencies within the sets of the requirements, to avoid non-compliance, contradictions and redundancies; (2) corresponding systematic process for change management in the case of global system development.

We introduce a framework for visualization of data originating from industrial automation devices. Our framework uses cloud-based services to collect data from industrial automation controllers. Clients can subscribe to the data sources and visualize them in accordance with customer needs. Data from industrial automation facilities is associated with formal semantic models, such as a mathematical representation of the material flow in a production plant. The formal models are used to represent interdependencies between entities, their functionality and other descriptive elements. Ultimately this is used in the visualization and for reasoning about systems. In addition to the software framework we describe work on our demonstrator: An example factory with Raspberry Pi-based controllers that are interconnected via standard ethernet technology.

This paper presents an approach for modelling and implementation of autonomous humanoid system’s behaviour. The main objective of our project was to analyse possible interaction scenarios between humans and autonomous robots, and to elaborate a framework for providing flexible guided tour options, utilising the features of humanoid PAL REEM robot. The framework can be used to support guided tours through exhibitions, museums, art centres, innovative labs, etc. We introduce the core results of the project and briefly discuss our future work. There are many scenarios where humans interactively conduct some joint activities. Using our approach, presented here, one of the parties could be replaced by humanoid robots. State of the art technology in voice recognition and generation, as well as path planning were used to achieve requested research objectives.

Cloud computing provides a great opportunity for scientists, as it enables large-scale experiments that cannot are too long to run on local desktop machines. Cloud-based computations can be highly parallel, long running and data-intensive, which is desirable for many kinds of scientific experiments. However, to unlock this power, we need a user-friendly interface and an easy-to-use methodology for conducting these experiments. For this reason, we introduce here a formal model of a cloud-based platform and the corresponding opensource implementation. The proposed solution allows to conduct experiments without having a deep technical understanding of cloud-computing, HPC, fault tolerance, or data management in order to leverage the benefits of cloud computing. In the current version, we have focused on biophysics and structural chemistry experiments, based on the analysis of big data from synchrotrons and atomic force microscopy. The domain experts noted the time savings for co mputing and data management, as well as user-friendly interface.

This paper presents an approach for an intelligent speed validation and adaptation. The approach focuses on formal modelling of the corresponding smart vehicle units, to increase the road safety as well as to allow formal analysis of the smart vehicle behaviour. We suggest a number of models for speed check/limitation units, which reflect differences in the speed limits in several countries. We also present our results from the case studies, based on two implementations of the model as an iOS and an Android app for Intelligent Speed Adaptation.

We propose a model-driven development approach for autonomous control systems with emphasis on the physical space and the communication via wireless connections. In particular, we combine model-based engineering with simulation and emulation techniques for mobile communication. The design and implementation is done using our Reactive Blocks Framework. For the mobile communication we use the popular IEEE 802.11 WLAN protocol which is simulated using software tools in order to get estimations of connection delays. The spatial constraints are verified with our Be Spaced tool. As an example, we present the design and verification of autonomous robots performing services in a large factory hall and coordinating by means of wireless communication which is based on several access points.

We present work towards a toolchain that combines our existing tools Reactive Blocks and BeSpaceD with our remote collaboration and visualization facility VxLab. Software development in areas such as oil and gas, mining or automation is subject to remote configuration and maintenance of installations. Different reasons are driving this trend including difficult accessibility of remote sites and outsourcing to offsite experts or due to cheaper labor costs. Here, we concentrate on work towards remote configuration, installation and maintenance of the software controlling these installations and their spatial constraints.

We present our ongoing work on requirements specification and analysis for the geographically distributed software and systems. Developing software and systems within/for different countries or states or even within/for different organisations means that the requirements to them can differ in each particular case. These aspects naturally impact on the software architecture and on the development process as a whole. The challenge is to deal with this diversity in a systematic way, avoiding contradictions and non-compliance. In this paper, we present a formal framework for the analysis of the requirements diversity, which comes from the differences in the regulations, laws and cultural aspects for different countries or organisations. The framework also provides the corresponding architectural view and the methods for requirements structuring and optimisation.

We present our monitoring and decision framework for collaborative engineering for globally distributed operation, support, maintenance, and services for industrial automation. The framework provides relevant information to plant operators, engineers, staff and stakeholders to support the handling of incidents, based on semantically-appropriate factors such as personnel skills, physical location of affected equipment and dependencies between plant elements. We discuss the proposed application and present the architecture and implementation. Based on incoming events the framework selects, aggregates and displays information automatically for human processing possibly at distant control centres. For example an alarm in a manufacturing facility can trigger the display of relevant information on multiple devices such as workstations, tablets, or large control-room screens to supervisors and experts. Devices can be potentially in different locations and can comprise different visualization capabilities. The core of our framework uses semantic models and formal methods-based techniques to aggregate and process this information.

The Virtual eXperiences Lab at RMIT is a “21st century lab scope,” an enabling platform for research and prototyping in industrial automation, focusing on software engineering, next generation human-machine interaction experiences, user interfaces, and training. VxLab combines high resolution visualization, industrial automation facilities and cloud-based simulation servers in a dedicated private network. In this paper we describe the architecture, use cases, and research and innovation projects. We also present experiences applying VxLab. We present capabilities, include connected infrastructure provided by industry partners.

Cyber-physical Systems (CPS) combine human-machine interaction, the physical world around us, and software aspects by integrating physical systems with communication networks. Opportunities and research challenges are largely interconnected with the three core sub-domains of CPS — computation, communication and control. The current state of the art of the legacy communication technology is one of the major hindrances limiting the evolution of CPS. Most specifically, innovation in communication is restricted with existing routing and switching technologies leaving no practical methods for researchers to test their new ideas. Software Defined Networking (SDN), through the realization of OpenFlow, separates network control logic from the underlying physical routers and switches. This phenomenon allows researchers to write high-level control programs specifying the behavior of the core networks used to implement CPS and thus, enable innovation in next generation communication architectures for CPS. In this paper, we propose a SDN architecture for industrial automation. Network design requirements are extracted from formal component specifications which support the generation of automatic network configurations. The proposed SDN architecture aims to leverage Industry 4.0 and Smart Factories, to bring together industrial automation installations with networking and Internet technologies.

This paper presents a formal model for science clouds, capable of predicting and controlling resources scalably, as well as its implementation as an open source solution, called Chiminey. The feasibility of Chiminey is shown using case studies on biophysics and structural chemistry computations. Big data is acquired from scientific instruments such as synchrotrons and atomic force microscopes. The model takes into account the architecture of the overall parallel and distributed system including large-scale data sources; data sinks, for example petabyte research data stores; and cluster or cloud virtual resources and infrastructures characterised by users in simple parameters upfront. Chiminey is developed to control large numbers of processes and to provide a reliable computing and data management, which can be used by researchers without having to learn extensive infrastructure concepts and technologies.

In many cases we need to represent on the same abstraction level not only system components but also processes within the system, and if for both representation different frameworks are used, the system model becomes hard to read and to understand. We suggest a solution how to cover this gap and to reconcile component and process views on system representation: a formal framework that gives the advantage of solving design problems for large-scale component systems.

The enabling of scientific experiments that are embarrassingly parallel, long running and data-intensive into a cloud-based execution environment is a desirable, though complex undertaking for many researchers. The management of such virtual environments is cumbersome and not necessarily within the core skill set for scientists and engineers. We present here Chiminey, a software platform that enables researchers to (i) run applications on both traditional high-performance computing and cloud-based computing infrastructures, (ii) handle failure during execution, (iii) curate and visualise execution outputs, (iv) share such data with collaborators or the public, and (v) search for publicly available data.

This paper presents an approach towards intelligent route planning in public transport systems. The approach focuses on formal modelling of the semi-dynamic intelligent route planning and optimisation. For these purposes, it is essential to have a well de- veloped formal model covering real-time and space aspects. The proposed solution allows designers to extend a public transport system with additional routes, which are created dynamically based on the requests from passengers. The model can be applied within a sustainable Smart City both for (fully or partially) autonomous transport systems and for the decision support systems of a smart transport system.

This paper presents a formal approach to modelling and analysis of data and control flow dependencies between services within remotely deployed distributed systems of services. Our work aims at elaborating for a concrete system, which parts of the system (or system model) are necessary to check a given property. The approach allows services decomposition oriented towards efficient checking of system properties as well as analysis of dependencies within a system.

We describe our ongoing work and view on simulation, validation and visualization of cyber-physical systems in industrial automation during development, operation and maintenance.System models may represent an existing physical part -for example an existing robot installation -and a software simulated part -for example a possible future extension.We call such systems cyber-virtual systems.In this paper, we present the existing VITELab infrastructure for visualization tasks in industrial automation.The new methodology for simulation and validation motivated in this paper integrates this infrastructure.We are targeting scenarios, where industrial sites which may be in remote locations are modeled and visualized from different sites anywhere in the world.Complementing the visualization work, here, we are also concentrating on software modeling challenges related to cyber-virtual systems and simulation, testing, validation and verification techniques for them.Software models of industrial sites require behavioural models of the components of the industrial sites such as models for tools, robots, workpieces and other machinery as well as communication and sensor facilities.Furthermore, collaboration between sites is an important goal of our work.

We present work towards using ontological information to facilitate collaborative tasks during operation, maintenance and service of industrial automation facilities. We use semantic models as an additional layer for a collaboration framework to enable automatic reasoning, decision support and knowledge sharing among multiple parties. Documents such as texts, workflows, images, social media profiles or models of production plants can be semantically annotated to facilitate their ontological classification. Our semantic models comprise behavior and space information, as well as links between documents and from documents to external data collections, such as logs, tables and sensor data. Our semantic models can be used to check consistency, confidentiality and security properties and to support collaborative tasks.

Failure in grids is costly and inevitable. Existing fault tolerance (FT) mechanisms are typically defensive and reactive, thus unnecessarily costly. In this paper we propose a hybrid FT approach, recovery aware component (RAC), combining reactive and proactive FT, with failure recovery or aversion of user-defined granularity, by component-orientation and architecture-level reasoning about FT, to increase reliability and availability without needless performance sacrifices. We model and analyse a parameterised RAC implementation combining prediction, proactive rejuvenation and reactive restarting to varying extents, calculating cost savings, reliability improvements and cost-benefit, under parameters such as prediction frequency and accuracy.

Programming languages provide exception handling mechanisms to structure fault tolerant activities into software systems. However, the use of exceptions at this low level of abstraction can be error-prone and complex leading to new programming errors. In this paper, we present a model-driven framework to support the iterative development of reliable software systems. This framework is comprised of UML-based modeling notations and a transformation engine that supports the automated generation of exception management features for a software system. It leverages domain specific exception modeling languages, patterns, modeling tools and framework libraries. The feasibility of this approach is demonstrated through the development of a case study business application, known as Project Tracker

Understanding nonfunctional aspects of system behavior is an essential component of practical software development and maintenance. Many nonfunctional system properties, such as reliability and availability, involve time and probabilities. In this paper, we present a framework for runtime verification and prediction of timed and probabilistic nonfunctional properties of component-based architectures, built using the Meta-Object Facility and the Distributed Management Task Force's Common Information Model (CIM) standard. We describe a Microsoft .NET-based implementation of our framework. We define a language for describing timed probabilistic behavior based on Probabilistic Computational Tree Logic (PCTL). We provide a formal semantics for this language in terms of observed application execution traces. The semantics is interesting in that it permits checking of required timing behavior both over the overall average of traces and also over local "trends" in traces. The latter aspect of the semantics is achieved by incorporating exponential smoothing prediction techniques into the truth function for statements of our language. The semantics is generic over the aspects of an application that are represented by states and state transitions. This enables the language to be used to describe a wide range of nonfunctional properties for runtime verification and prediction purposes. We explain how statements of our language are used to define precise contracts for system monitoring, through relating the semantics to an extended CIM monitoring infrastructure.

Because of computational grid heterogeneity, scale and complexity, faults become likely. Therefore, grid infrastructure must have mechanisms to deal with faults while also providing efficient and reliable services to its end users. Existing fault-tolerant approaches are inefficient because they are reactive and incomplete. They are reactive because they only deal with faults when they take place; they are incomplete because they only deal with certain types of faults. Proactive approaches increase efficiency by reducing the cost and time of operations and network resource usage by maintaining the state of executing applications and resuming operation when rescheduled. This paper presents an agent oriented, fault-tolerant grid framework where agents deal with individual faults proactively. Agents maintain information about hardware conditions, executing process memory consumption, available resources, network conditions and component mean time to failure. Based on this information and critical states, agent can improve the reliability and efficiency of grid services.

It is now recognized that nonfunctional properties are important to practical software development and maintenance. Many of these properties involve time and probabilities - for example, reliability and availability. In this paper, we present a framework for runtime verification of timed and probabilistic nonfunctional properties of component-based architectures, built using the meta-object facility and the Distributed Management Task Force's common information model (CIM) standard. We describe a Microsoft .NET-based implementation of our framework. We use a language for contracts based on probabilistic computational tree logic (PCTL). We provide a formal semantics for this language based on possible application execution traces. The semantics is parametrized with respect to the choice of application states and state changes to be monitored. This enables us to use the language to define a wide range of nonfunctional properties. We explain how our framework associates constraints with systems that expose management information through the CIM, via a novel extension of the CIM metamodel.

This report gives an overview of the 6th ICSE Workshop on Component-Based Software Engineering held at 25th International Conference on Software Engineering. The workshop brought together researchers and practitioners from three communities: component technology, software architecture, and software certification. The primary goal of the workshop was to continue clarifying the concepts, identifying the main challenges and findings of predictable assembly of certifiable software components. This report gives a comprehensive summary of the position papers, of the workshop, its findings, and its results.

This workshop brings together researchers and practitioners from the community interested in predictable assembly from certifiable components. The goal of this workshop is to ensure continued collaboration among the members of this community. One output of the workshop will be an understanding of composition theory and how it applies to community model problems that were suggested at the workshop on component-based software engineering held at ICSE in 2001. A second output will be the identification of research opportunities that lie on the perimeter of predictable assembly.

Time management in workflow processes is crucial in determining and controlling the life cycle of business activities. In our model, a temporal interval as an execution duration is assigned to every workflow task. While the real time taken by the task is nondeterministic and unpredictable, it may be between the bounds thus specified. We extend workflow nets (WF-nets) with time intervals and call the new nets Time WF-nets (TWF-nets). Extending our previous results on timed Petri nets, we show that certain behavioural properties of workflow processes modelled in TWF-nets can be verified. Using a clinical health care process as a case study, we also illustrate the modelling of shared resources available at different times.

Call centers are at the core of today's customer relations management. Increasingly, they are also utilized internally as competence and knowledge centers. Turning them into service centers of the future (SCotF) requires parallel communication over several channels, including Internet services, in a distributed synchronous fashion. In this paper, we show that the emerging XML standards provide a good basis for this type of interaction. In turning e-service into a groupware application, we propose to apply a spatial awareness model to assist in the collaboration. We demonstrate that it can be integrated into the XML/XSL-framework. The results are compared with a previous solution, which applied proprietary tools. Questions of fidelity and a critique of the existing standards and tools complement the practical results.

The paper presents a scheduling system, Schedular++, which integrates logic rules into the object oriented paradigm. Schedular++ demonstrates the application of knowledge objects to solve a scheduling problem. Telecom manages the telephone network across the entire country. To efficiently manage the network, many fault dispatch centres (FDC) are distributed across the country, and each FDC maintains a team of field workers to fix faults in several of their service suburbs. One of the daily jobs in each FDC is to dispatch workers to fix network faults in each suburb. This includes daily downloading of defect reports from the customer service representatives' (CSR) database (CSR is the operator service where customers call for their telephone defects), and schedule workers for the next day. Consideration is given to building an object oriented system to schedule workers to faults in each FDC. Rules should be incorporated into this system to provide better constraints representation and inference ability to the system.

Inheritance Anomaly is considered as a major problem in integrating object-orientation and concurrency. The anomaly forces redefinitions of inherited methods to maintain the integrity of concurrent objects. In this paper we discuss how the use of boolean, access and path guards attached to methods solve the problem of inheritance anomaly. Synchronization using boolean guards have known to be free of inheritance anomaly caused by partitioning of acceptable states. However, they cause anomalies from history sensitivity. We solve this using path guards. Path guards are similar to path expressions in the sense that both express the execution pattern of methods. However while a path expression independently specifies the synchronization of a collection of methods, a path guard is attached to a method and it specifies the history of execution sequence(s) acceptable for executing the current method. Path expressions have been shown to cause inheritance anomaly, on the other hand, we will show that path guards form a solution to the problem.

Embedded specifications in object-oriented (OO) languages such as Eiffel and Sather are based on a rigorous approach towards validation, compatibility and reusability of sequential programs. The underlying method of "design-by-contract" is based on Hoare logic for which concurrency extensions exist. However concurrent OO languages are still in their infancy. They have inherently imperative facets, such as object identity, sharing, and synchronisation, which cannot be ignored in the semantics. Any marriage of objects and concurrency requires a trade-off in a space of intertwined qualities. The paper summarises our work on a type system, calculus and an operational model for concurrent objects in a minimal extension of the Eiffel and Sather languages (cSather). We omit concurrency control constructs and instead use assertions as synchronisation constraints for asynchronous functions. We show that this provides a framework in which subtyping and concurrency can coexist.