Abstract
In the domain of machines' design, one of the most important issues to solve is related with the controller's design, mainly, guaranteeing that the machine will behave as expected. In order to achieve a dependable controller, some steps can be considered, such as the formalization of its specification-before being translated to the program that will be inserted in the controller device-and the respective analysis and verification. Nowadays, some formal analysis techniques, such as formal verification, are used to achieve this purpose. The dependability of a controller, however, is impacted by its execution context. This paper proposes an approach for the formal verification of the specification of mechatronic system's controllers, which considers, on the formal verification tasks, the behavior of the plant and the behavior of the Human Machine Interface of the Mechatronic system. Some conclusions are extrapolated for other systems of the same kind.

Abstract
As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics used to express the properties of a system's behaviour is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process. Errors in this step of the process can create serious problems since a false sense of safety is gained from the analysis. However, when compared to the effort put into developing and applying modelling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. In this paper we illustrate how a collection of property patterns can help in simplifying the process of generating logical formulae from informally expressed requirements.

Abstract
Model-based methodologies, supported by automatic generation, have been proposed as a solution to reduce software development costs. In the case of interactive computing systems specific challenges arise. On the one hand, a high level of automation requires the use of detailed models, which is contrary to the iterative development process, based on the progressive refinement of user interface mockups, typical of user centered development processes. On the other hand, layered software architectures imply a distinction between the models used in the business logic and in the user interface, raising consistency problems between the models at each level. This article proposes a tool supported approach to user interface generation directly from the architectural models of the business logic. In many situations, user interfaces provide similar features inside a specific domain. The identification of the application domain is thus a key factor in supporting the automation of the generation process. © 2017 Association for Computing Machinery.

Abstract
Ensuring that an interactive application allows users to perform their activities and reach their goals is critical to the overall usability of the interactive application. Indeed, the effectiveness factor of usability directly refers to this capability. Assessing effectiveness is a real challenge for usability testing as usability tests only cover a very limited number of tasks and activities. This paper proposes an approach towards automated testing of effectiveness of interactive applications. To this end we resort to two main elements: An exhaustive description of users’ activities and goals using task models, and the generation of scenarios (from the task models) to be tested over the application. However, the number of scenarios can be very high (beyond the computing capabilities of machines) and we might end up testing multiple similar scenarios. In order to overcome these problems, we propose strategies based on task models manipulations (e.g., manipulating task nodes, operator nodes, information...) resulting in a more intelligent test case generation approach. For each strategy, we investigate its relevance (both in terms of test case generation and in terms of validity compared to the original task models) and we illustrate it with a small example. Finally, the proposed strategies are applied on a real-size case study demonstrating their relevance and validity to test interactive applications. © 2017 Association for Computing Machinery.

Abstract

Abstract
User centred design approaches typically focus understanding on context and producing sketch designs. These sketches are often non functional (e.g., paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The sketch design of a device is enhanced into a specification that is then analysed using formal techniques, thus providing a systematic approach to checking plausibility and consistency during early design stages. Once analysed, a further prototype is constructed using an executable form of the specification, providing the next candidate for evaluation with potential users. The technique is illustrated through an example based on a pill dispenser. © Springer Nature Switzerland AG 2018.