Abstract
This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call D-down arrow-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems.

Abstract
In several countries, it is a common practice for construction owners to require contractors to submit several types of surety bonds shifting the risk of contractors default to sureties. The process of evaluating contractors' applications for bonding is complicated and time-consuming. Surety underwriters are faced with the challenge of considering tens of objective and subjective criteria to make the bonding recommendation. These criteria include a contractor's financial strength, past performance, and other related aspects. Literature review revealed that there is little guidance to surety underwriters in this regard. As a result, the purpose of this paper is to equip surety underwriters with a decision making model for evaluating contractors' applications for bonding. The proposed model is based on data envelopment analysis (DEA). The DEA is a robust nonparametric linear programming approach that is widely used for benchmarking, performance measurement, and decision making. The proposed DEA model guides surety underwriters throughout the decision making process. The model offers surety underwriters the flexibility to accommodate any number of variables in the evaluation process. The proposed model is deployed based on a database that includes 49 contractors. The validity and applicability of the proposed model are scored positively by industry practitioners in terms of methodology used, evaluation criteria, ease of use, performance results, and overall usefulness compared to existing methods. (C) 2015 American Society of Civil Engineers.

Abstract
This descriptive study explores the state of CSR education and research in Portugal. It aims to depict the state of CSR in Portugal, in particular in what concerns the nature and the extent of education and research on CSR being undertaken in Portugal. The methodology used includes analysis of relevant literature and of business schools’ websites, and a survey by questionnaire among students at the business school at which the authors of this chapter teach and research. In terms of CSR practices, there is still some focus on social issues, given the state of development of the Portuguese economy. There are signs of CSR having reached a reasonable level of maturity. Although CSR education and research seem to be reasonably well developed in the leading business schools, the same is not the case with other schools. Research on CSR is concentrated in the schools in which CSR education is more developed.

Abstract
This paper presents a new approach to an audio-based indoor localization system. By using audio signals emitted by a public address sound system, mobile devices may globally localize themselves in an indoor environment where global navigation satellite systems are not viable or reliable. The use of data hiding techniques such as spread spectrum coding or echo hiding has allowed to convey information to a receiver avoiding people’s perception of the added audio content. Results demonstrate a relatively quite good localization with centimetre accuracy and precision and successful data transmission using barely perceptible audio signals.

Abstract
The progress in medical science and the decline of altruistic behavior of couples introduced to the world the ageing problem. The existence of ageing is more experienced by developed countries. Researchers and policy makers are constantly trying to find ways to study the impacts of ageing since the issue is unprecedented in our history. However, the majority of the literature focus more on immediate mechanisms such as public expenditures and somehow neglected the influence of ageing on manufacturing sector. Thus, through panel data, we studied the influence of ageing on manufacturing sectors. The empirical study was carried out on six developed countries namely Japan, Germany, Italy, Greece, Finland and Portugal that have high ageing population. Our results suggest that the growth of the old age group over 65 years old will have significantly negative influence on percentage contribution of manufacturing to the GDP of these countries. Moreover, the results also demonstrate that a country with a higher proportion of old age group over working group will face fall in the manufacturing.

Abstract
In order to achieve underwater acoustic high data-rate and real time communications, it is essential to implement a system that operates both at high and wideband frequencies using digital modulations. Therefore, to reduce the time and cost of developing acoustic communications an emulator of a physical layer model was implemented, allowing to test in real time the performance of digital modulations. The model was composed of an emitter transducer, a hydrophone and the subaquatic medium and was integrated in a Field Programmable Gate Array (FPGA) in order to emulate the physical layer in the acoustic modem testing. The emitter transducer and the hydrophone models were designed to meet real prototype characteristics. The system prototype was implemented in order to compare the experimental trials results with those obtained in emulator, emulating the transmission of acoustic signals, using different types of digital modulations. The system was tested using Binary Phase-Shift Keying (BPSK), Binary Frequency Shift keying (BFSK) and Binary Amplitude Shift Keying (BASK) modulations with a 1 MHz carrier frequency resulting in a data rate of 125 kbps. It was verified that the implemented model represents a suitable approximation to the real subaquatic communication channel, allowing the evaluation of digital acoustic communications.