The use of the UML specification language is very widespread due to some of its features. However, the ever more complex systems of today require modeling methods that allow errors to be detected in the initial phases of development. The use of formal methods make such error detection possible but the learning cost is high.This paper presents a tool which avoids this learning cost, enabling the active behavior of a system expressed in UML to be verified in a completely automatic way by means of formal method techniques. It incorporates an assistant for the verification that acts as a user guide for writing properties so that she/he needs no knowledge of either temporal logic or the form of the specification obtained

The ability to know the precise level of occupancy in an indoor or outdoor space in real time could have multiple applications. It is a well-known problem for which a number of technologies have been proposed over time. The recent emergence of BLE beacon technology has provided a solution to the problem. This study presents a tool that uses beacons and user smartphones to determine the level of occupancy in indoor and outdoor spaces, providing real-time information that can be published as open data and subsequently used by other applications. The tool was tested in a university environment in real-life situations and has produced promising results in obtaining an occupancy count.