The file attached to this record is the author's final peer reviewed version. Smart Home Systems (SHSs) provide several services which are tailored to different residents’ preferences. As a result, SHSs are highly exposed to undesirable interactions, known as feature interactions (FIs). FIs might occur as a result of a conflict in services’ goals or a conflict with residents’ preferences. Previous studies have proposed solutions based on applying priorities, in which some services or preferable features are disabled in favour of other services. Alternatively, the agent-based negotiation approach (ABNA) utilises agents and applies negotiation, enabling services with contrary features to work simultaneously. ABNA avoids applying priority between services or house residents’ preferences whenever a space for a compromise exists. The mechanism of ABNA is based on the use of a hierarchy of features based on their contribution to the function of the service or on the importance of these features to house residents. To achieve a compromise between conflicting services, ABNA models services and residents by using agents, and implements a negotiation algorithm that allows services with conflicting features to work simultaneously. This paper presents a description of ABNA with a formal specification of ABNA in the Calculus of Context-aware Ambient (CCA). This enables the formal analysis of ABNA by using the execution environment of CCA.
