Towards deductive-based support for software development processes

The work relates two initial disciplines of the Rational Unified Process (RUP), i.e. Business Modeling and Requirements Engineering, to support them in an integrated way through deductive-based formal verification using temporal logic. On the other hand, Cyber-Physical Systems (CPS), which should be an effective orchestration of computations and physical processes, need careful development and formal verification to ensure they influence software reliability, trustworthiness and cost in a positive way. A method for building both business models and requirements models, including their logical specifications, is proposed and presented step by step. Applying the presented concepts bridges the gap between the benefits of deductive reasoning for correctness analysis and the difficulties in obtaining complete logical specifications.