随着Internet广泛应用和普及,软件开发、部署、运行和维护的计算平台已经逐步由封闭、静态、可控走向开放、动态、难控。Internet平台上软件系统已经呈现为柔性可演化、连续反应式、多目标适应的新形态。中国软件工程领域将这样一种新的软件形态称之为网构软件。本文对网构软件的构造过程以及网构软件整个生命周期进行研究,基于抽象状态机理论提出一套适合分析、构造以及验证可靠网构软件系统的形式化模型,同时给出普适环境下智能家庭系统的原型案例。论文的主要研究工作和创新性包含以下几个方面:(1)本文采用分布式抽象状态机进行刻画目标网构软件系统,建立分布式抽象状态机与网构软件之间的映射关系,在这个模型中每个子抽象状态机对应为网络平台中的一个构件,而构件内部的输入输出又进一步分解成子抽象状态机,它们之间通过监督函数进行交互。在该环境中,除了构件本身,其它所有与此构件有交互关系的构件及网络状况都构成了该构件的运行环境。环境中的普通函数通过成为该构件子状态机中的监督函数来对该构件提供环境信息。通过这些映射关系,建立了基于抽象状态机的网构软件模型。该模型具有可抽象执行验证的特征,使得目标系统在需求高抽象层次各种属性能够得到验证。在模型中对构件之间的交互模式,交互仲裁模型等进行了详细的分析,该模型的建立使得网构软件在构造之前需求能够准确清晰。(2)由于采用抽象状态机刻画网构软件系统往往从抽象程度极高的自然层次开始,为了使模型能够逐步向可执行的目标系统逼近,本文提出基于抽象状态机网构软件抽象模型的精化机制,并给出交互模式的精化模型和构件精化模型。通过研究基于抽象状态机网构软件抽象模型的通用精化机制,本文进一步给出了智能家庭体系结构中协作模型的精化模型以及基于OSGi的普适网构基础平台的精化模型。在这些模型中保证了精化步骤不丢失或变化系统的原有特性和性质,从而确保精化的正确性,最终保证高层次抽象网构软件模型与最终网构软件模型的一致性。(3)为了在网构软件设计的早期阶段尽量的避免和消除错误,本文采用抽象状态机的可抽象执行机制,提出网构软件精化设计过程中在不同抽象层次的可执行验证模型。因此,通过该模型可以在不同的抽象层次对网构软件设计模型进行模拟执行,从而尽早的发现设计中的问题,在设计的早期阶段保证软件的正确性,避免后期错误带来的巨大损失。另一方面,为了在设计的精化过程中不丢失目标系统的各种属性,精化前后保持一致性,本文提出了基于抽象状态机的网构软件模型精化验证模型,通过该模型能够确保设计精化过程的正确性,由此也可以由过程的正确性来保证目标系统的正确性。(4)为了采用网构软件理论有效的解决普适计算领域中的问题以及使网构软件理论在新的领域进一步得到验证和丰富,本文采用OSGi和R-OSGi作为普适网构软件平台,并提出合理的智能家庭体系结构。在该结构中,结合R-OSGi技术优点给出了三种重要的协作模型:a)直接服务请求协作模型,b)基于远程事件的发布/订阅形成的协作模型,c)被动协作模型,并且在原型系统中得到了实现。通过系统实验验证可以看出,本体系结构对于指导普适网构软件的开发具有一定现实意义。