Determining Software Models That Are Less Incorrect

We describe our theoretical behavioral modeling research in specific domains where finite-state models really can be found. There, with precise model-based design and perfect model checking, we obtain correct results by constructive inference, adequate testing and verification. In actual software develop-ment we find these results can only approximately apply. Still we show they can assist in software design that is “less incorrect”, consistent with the results of theoreticians and practitioners working in actual model-based design and model checking. Introduction: Our Approach to Modeling Model-based software design is a formal approach to de-veloping better specifications and thus, better software. Model checkers, on the other hand, are formal tools tha